Documentation

Arithmetization.Vorspiel.Lemmata

Instances
    theorem LO.FirstOrder.Structure.Monotone.monotone {L : LO.FirstOrder.Language} {M : Type u_1} [LE M] [LO.FirstOrder.Structure L M] [self : LO.FirstOrder.Structure.Monotone L M] {k : } (f : L.Func k) (v₁ : Fin kM) (v₂ : Fin kM) :
    (∀ (i : Fin k), v₁ i v₂ i)LO.FirstOrder.Structure.func f v₁ LO.FirstOrder.Structure.func f v₂
    theorem LO.FirstOrder.Structure.Monotone.term_monotone {L : LO.FirstOrder.Language} {M : Type u_1} [LE M] [LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Monotone L M] {ξ : Type u_2} {n : } (t : LO.FirstOrder.Semiterm L ξ n) {e₁ : Fin nM} {e₂ : Fin nM} {ε₁ : ξM} {ε₂ : ξM} (he : ∀ (i : Fin n), e₁ i e₂ i) (hε : ∀ (i : ξ), ε₁ i ε₂ i) :
    def LO.FirstOrder.Semiterm.arithCases {ξ : Type u_1} {n : } {C : LO.FirstOrder.Semiterm ℒₒᵣ ξ nSort w} (hbvar : (x : Fin n) → C (LO.FirstOrder.Semiterm.bvar x)) (hfvar : (x : ξ) → C (LO.FirstOrder.Semiterm.fvar x)) (hzero : C (‘0’)) (hone : C (‘1’)) (hadd : (t u : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) → C (‘(!!t + !!u)’)) (hmul : (t u : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) → C (‘(!!t * !!u)’)) (t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) :
    C t
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[irreducible]
      def LO.FirstOrder.Semiterm.arithRec {ξ : Type u_1} {n : } {C : LO.FirstOrder.Semiterm ℒₒᵣ ξ nSort w} (hbvar : (x : Fin n) → C (LO.FirstOrder.Semiterm.bvar x)) (hfvar : (x : ξ) → C (LO.FirstOrder.Semiterm.fvar x)) (hzero : C (‘0’)) (hone : C (‘1’)) (hadd : {t u : LO.FirstOrder.Semiterm ℒₒᵣ ξ n} → C tC uC (‘(!!t + !!u)’)) (hmul : {t u : LO.FirstOrder.Semiterm ℒₒᵣ ξ n} → C tC uC (‘(!!t * !!u)’)) (t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) :
      C t
      Equations
      Instances For
        Equations
        • =
        theorem LO.Arith.lt_succ_iff_le {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {x : M} {y : M} :
        x < y + 1 x y
        theorem LO.Arith.lt_iff_succ_le {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} :
        a < b a + 1 b
        theorem LO.Arith.succ_le_iff_lt {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} :
        a + 1 b a < b
        theorem LO.Arith.pos_iff_one_le {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :
        0 < a 1 a
        theorem LO.Arith.one_lt_iff_two_le {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :
        1 < a 2 a
        @[simp]
        theorem LO.Arith.not_nonpos {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (a : M) :
        ¬a < 0
        theorem LO.Arith.lt_two_iff_le_one {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :
        a < 2 a 1
        @[simp]
        theorem LO.Arith.lt_one_iff_eq_zero {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :
        a < 1 a = 0
        @[simp]
        theorem LO.Arith.le_mul_self {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (a : M) :
        a a * a
        @[simp]
        theorem LO.Arith.le_sq {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (a : M) :
        a a ^ 2
        @[simp]
        theorem LO.Arith.sq_le_sq {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} :
        a ^ 2 b ^ 2 a b
        @[simp]
        theorem LO.Arith.sq_lt_sq {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} :
        a ^ 2 < b ^ 2 a < b
        theorem LO.Arith.le_mul_of_pos_right {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} (h : 0 < b) :
        a a * b
        theorem LO.Arith.le_mul_of_pos_left {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} (h : 0 < b) :
        a b * a
        @[simp]
        theorem LO.Arith.le_two_mul_left {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :
        a 2 * a
        theorem LO.Arith.lt_mul_of_pos_of_one_lt_right {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} (pos : 0 < a) (h : 1 < b) :
        a < a * b
        theorem LO.Arith.lt_mul_of_pos_of_one_lt_left {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} (pos : 0 < a) (h : 1 < b) :
        a < b * a
        theorem LO.Arith.mul_le_mul_left {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} {c : M} (h : b c) :
        a * b a * c
        theorem LO.Arith.mul_le_mul_right {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} {c : M} (h : b c) :
        b * a c * a
        theorem LO.Arith.lt_of_mul_lt_mul_left {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} {c : M} (h : a * b < a * c) :
        b < c
        theorem LO.Arith.lt_of_mul_lt_mul_right {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} {c : M} (h : b * a < c * a) :
        b < c
        theorem LO.Arith.pow_three {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
        x ^ 3 = x * x * x
        theorem LO.Arith.pow_four {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
        x ^ 4 = x * x * x * x
        theorem LO.Arith.pow_four_eq_sq_sq {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
        x ^ 4 = (x ^ 2) ^ 2
        def LO.Arith.instCovariantClassHMulLe_arithmetization {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :
        CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x x_1
        Equations
        • =
        Instances For
          def LO.Arith.instCovariantClassHAddLe_arithmetization {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :
          CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x x_1
          Equations
          • =
          Instances For
            def LO.Arith.instCovariantClassSwapHMulLe_arithmetization {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :
            CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x x_1
            Equations
            • =
            Instances For
              @[simp]
              theorem LO.Arith.one_lt_mul_self_iff {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :
              1 < a * a 1 < a
              @[simp]
              theorem LO.Arith.opos_lt_sq_pos_iff {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :
              0 < a ^ 2 0 < a
              @[simp]
              theorem LO.Arith.one_lt_sq_iff {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :
              1 < a ^ 2 1 < a
              @[simp]
              theorem LO.Arith.mul_self_eq_one_iff {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :
              a * a = 1 a = 1
              @[simp]
              theorem LO.Arith.sq_eq_one_iff {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :
              a ^ 2 = 1 a = 1
              theorem LO.Arith.lt_square_of_lt {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} (pos : 1 < a) :
              a < a ^ 2
              theorem LO.Arith.two_mul_le_sq {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {i : M} (h : 2 i) :
              2 * i i ^ 2
              theorem LO.Arith.two_mul_le_sq_add_one {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (i : M) :
              2 * i i ^ 2 + 1
              theorem LO.Arith.two_mul_lt_sq {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {i : M} (h : 2 < i) :
              2 * i < i ^ 2
              theorem LO.Arith.succ_le_double_of_pos {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} (h : 0 < a) :
              a + 1 2 * a
              theorem LO.Arith.two_mul_add_one_lt_two_mul_of_lt {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} {b : M} (h : a < b) :
              2 * a + 1 < 2 * b
              @[simp]
              theorem LO.Arith.le_add_add_left {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (a : M) (b : M) (c : M) :
              a a + b + c
              @[simp]
              theorem LO.Arith.le_add_add_right {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (a : M) (b : M) (c : M) :
              b a + b + c
              @[simp]
              Equations
              • LO.Arith.instMonotoneORing = { monotone := }
              @[simp]
              theorem LO.Arith.zero_ne_add_one {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
              0 x + 1
              @[simp]
              theorem LO.Arith.nat_cast_inj {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {n : } {m : } :
              n = m n = m
              @[simp]
              theorem LO.Arith.coe_coe_lt {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {n : } {m : } :
              n < m n < m
              theorem LO.Arith.coe_succ {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : ) :
              (x + 1) = x + 1

              TODO: move

              @[reducible, inline]
              Equations
              Instances For
                @[simp]
                theorem LO.Arith.natCast_nat (n : ) :
                n = n
                @[simp]