Foundation.Arithmetization.Vorspiel.Lemmata

class LO.FirstOrder.Structure.Monotone (L : Language) (M : Type u_1) [LE M] [Structure L M] :

monotone {k : ℕ} (f : L.Func k) (v₁ v₂ : Fin k → M) : (∀ (i : Fin k), v₁ i ≤ v₂ i) → func f v₁ ≤ func f v₂

Instances

LO.Arith.instMonotoneORing

theorem LO.FirstOrder.Structure.Monotone.term_monotone {L : Language} {M : Type u_1} [LE M] [Structure L M] [Monotone L M] {ξ : Type u_2} {n : ℕ} (t : Semiterm L ξ n) {e₁ e₂ : Fin n → M} {ε₁ ε₂ : ξ → M} (he : ∀ (i : Fin n), e₁ i ≤ e₂ i) (hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i) :

Semiterm.valm M e₁ ε₁ t ≤ Semiterm.valm M e₂ ε₂ t

source

def LO.FirstOrder.Semiterm.arithCases {ξ : Type u_1} {n : ℕ} {C : Semiterm ℒₒᵣ ξ n → Sort w} (hbvar : (x : Fin n) → C (bvar x)) (hfvar : (x : ξ) → C (fvar x)) (hzero : C ↑0) (hone : C ↑1) (hadd : (t u : Semiterm ℒₒᵣ ξ n) → C (‘(!!t + !!u)’)) (hmul : (t u : Semiterm ℒₒᵣ ξ n) → C (‘(!!t * !!u)’)) (t : Semiterm ℒₒᵣ ξ n) :

C t

Equations

LO.FirstOrder.Semiterm.arithCases hbvar hfvar hzero hone hadd hmul (LO.FirstOrder.Semiterm.bvar x_1) = hbvar x_1
LO.FirstOrder.Semiterm.arithCases hbvar hfvar hzero hone hadd hmul (LO.FirstOrder.Semiterm.fvar x_1) = hfvar x_1
LO.FirstOrder.Semiterm.arithCases hbvar hfvar hzero hone hadd hmul (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.zero a) = ⋯.mpr (⋯.mp hzero)
LO.FirstOrder.Semiterm.arithCases hbvar hfvar hzero hone hadd hmul (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.one a) = ⋯.mpr (⋯.mp hone)
LO.FirstOrder.Semiterm.arithCases hbvar hfvar hzero hone hadd hmul (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.add v) = ⋯.mp (hadd (v 0) (v 1))
LO.FirstOrder.Semiterm.arithCases hbvar hfvar hzero hone hadd hmul (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.mul v) = ⋯.mp (hmul (v 0) (v 1))

source

@[irreducible]

def LO.FirstOrder.Semiterm.arithRec {ξ : Type u_1} {n : ℕ} {C : Semiterm ℒₒᵣ ξ n → Sort w} (hbvar : (x : Fin n) → C (bvar x)) (hfvar : (x : ξ) → C (fvar x)) (hzero : C ↑0) (hone : C ↑1) (hadd : {t u : Semiterm ℒₒᵣ ξ n} → C t → C u → C (‘(!!t + !!u)’)) (hmul : {t u : Semiterm ℒₒᵣ ξ n} → C t → C u → C (‘(!!t * !!u)’)) (t : Semiterm ℒₒᵣ ξ n) :

C t

Equations

One or more equations did not get rendered due to their size.
LO.FirstOrder.Semiterm.arithRec hbvar hfvar hzero hone hadd hmul (LO.FirstOrder.Semiterm.bvar x_1) = hbvar x_1
LO.FirstOrder.Semiterm.arithRec hbvar hfvar hzero hone hadd hmul (LO.FirstOrder.Semiterm.fvar x_1) = hfvar x_1
LO.FirstOrder.Semiterm.arithRec hbvar hfvar hzero hone hadd hmul (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.zero a) = ⋯.mpr (⋯.mp hzero)
LO.FirstOrder.Semiterm.arithRec hbvar hfvar hzero hone hadd hmul (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.one a) = ⋯.mpr (⋯.mp hone)

source

instance LO.Arith.instNonempty_foundation {M : Type u_1} [ORingStruc M] :

Nonempty M

source

@[simp]

theorem LO.Arith.numeral_two_eq_two {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

ORingStruc.numeral 2 = 2

source

@[simp]

theorem LO.Arith.numeral_three_eq_three {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

ORingStruc.numeral 3 = 3

source

@[simp]

theorem LO.Arith.numeral_four_eq_four {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

ORingStruc.numeral 4 = 4

source

theorem LO.Arith.lt_succ_iff_le {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {x y : M} :

x < y + 1 ↔ x ≤ y

source

theorem LO.Arith.lt_iff_succ_le {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b : M} :

a < b ↔ a + 1 ≤ b

source

theorem LO.Arith.succ_le_iff_lt {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b : M} :

a + 1 ≤ b ↔ a < b

source

theorem LO.Arith.pos_iff_one_le {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

0 < a ↔ 1 ≤ a

source

theorem LO.Arith.one_lt_iff_two_le {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

1 < a ↔ 2 ≤ a

source

@[simp]

theorem LO.Arith.not_nonpos {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (a : M) :

¬a < 0

source

theorem LO.Arith.lt_two_iff_le_one {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

a < 2 ↔ a ≤ 1

source

@[simp]

theorem LO.Arith.lt_one_iff_eq_zero {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

a < 1 ↔ a = 0

source

theorem LO.Arith.le_one_iff_eq_zero_or_one {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

a ≤ 1 ↔ a = 0 ∨ a = 1

source

theorem LO.Arith.le_two_iff_eq_zero_or_one_or_two {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

a ≤ 2 ↔ a = 0 ∨ a = 1 ∨ a = 2

source

theorem LO.Arith.le_three_iff_eq_zero_or_one_or_two_or_three {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

a ≤ 3 ↔ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3

source

theorem LO.Arith.two_mul_two_eq_four {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

2 * 2 = 4

source

theorem LO.Arith.two_pow_two_eq_four {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

2 ^ 2 = 4

source

theorem LO.Arith.two_pos {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

0 < 2

source

@[simp]

theorem LO.Arith.le_mul_self {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (a : M) :

a ≤ a * a

source

@[simp]

theorem LO.Arith.le_sq {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (a : M) :

a ≤ a ^ 2

source

@[simp]

theorem LO.Arith.sq_le_sq {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b : M} :

a ^ 2 ≤ b ^ 2 ↔ a ≤ b

source

@[simp]

theorem LO.Arith.sq_lt_sq {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b : M} :

a ^ 2 < b ^ 2 ↔ a < b

source

theorem LO.Arith.le_mul_of_pos_right {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b : M} (h : 0 < b) :

a ≤ a * b

source

theorem LO.Arith.le_mul_of_pos_left {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b : M} (h : 0 < b) :

a ≤ b * a

source

@[simp]

theorem LO.Arith.le_two_mul_left {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

a ≤ 2 * a

source

theorem LO.Arith.lt_mul_of_pos_of_one_lt_right {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b : M} (pos : 0 < a) (h : 1 < b) :

a < a * b

source

theorem LO.Arith.lt_mul_of_pos_of_one_lt_left {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b : M} (pos : 0 < a) (h : 1 < b) :

a < b * a

source

theorem LO.Arith.mul_le_mul_left {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b c : M} (h : b ≤ c) :

a * b ≤ a * c

source

theorem LO.Arith.mul_le_mul_right {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b c : M} (h : b ≤ c) :

b * a ≤ c * a

source

theorem LO.Arith.lt_of_mul_lt_mul_left {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b c : M} (h : a * b < a * c) :

b < c

source

theorem LO.Arith.lt_of_mul_lt_mul_right {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b c : M} (h : b * a < c * a) :

b < c

source

theorem LO.Arith.pow_three {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

x ^ 3 = x * x * x

source

theorem LO.Arith.pow_four {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

x ^ 4 = x * x * x * x

source

theorem LO.Arith.pow_four_eq_sq_sq {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

x ^ 4 = (x ^ 2) ^ 2

source

theorem LO.Arith.instCovariantClassHMulLe_foundation {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2

source

theorem LO.Arith.instCovariantClassHAddLe_foundation {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2

source

theorem LO.Arith.instCovariantClassSwapHMulLe_foundation {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2

source

@[simp]

theorem LO.Arith.one_lt_mul_self_iff {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

1 < a * a ↔ 1 < a

source

@[simp]

theorem LO.Arith.opos_lt_sq_pos_iff {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

0 < a ^ 2 ↔ 0 < a

source

@[simp]

theorem LO.Arith.one_lt_sq_iff {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

1 < a ^ 2 ↔ 1 < a

source

@[simp]

theorem LO.Arith.mul_self_eq_one_iff {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

a * a = 1 ↔ a = 1

source

@[simp]

theorem LO.Arith.sq_eq_one_iff {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} :

a ^ 2 = 1 ↔ a = 1

source

theorem LO.Arith.lt_square_of_lt {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} (pos : 1 < a) :

a < a ^ 2

source

theorem LO.Arith.two_mul_le_sq {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {i : M} (h : 2 ≤ i) :

2 * i ≤ i ^ 2

source

theorem LO.Arith.two_mul_le_sq_add_one {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (i : M) :

2 * i ≤ i ^ 2 + 1

source

theorem LO.Arith.two_mul_lt_sq {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {i : M} (h : 2 < i) :

2 * i < i ^ 2

source

theorem LO.Arith.succ_le_double_of_pos {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a : M} (h : 0 < a) :

a + 1 ≤ 2 * a

source

theorem LO.Arith.two_mul_add_one_lt_two_mul_of_lt {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {a b : M} (h : a < b) :

2 * a + 1 < 2 * b

source

@[simp]

theorem LO.Arith.le_add_add_left {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (a b c : M) :

a ≤ a + b + c

source

@[simp]

theorem LO.Arith.le_add_add_right {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (a b c : M) :

b ≤ a + b + c

source

theorem LO.Arith.add_le_cancel {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (a : M) :

AddLECancellable a

source

@[simp]

theorem LO.Arith.val_npow {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (k : ℕ) (a : M) :

(FirstOrder.Semiterm.Operator.npow ℒₒᵣ k).val ![a] = a ^ k

source

instance LO.Arith.instMonotoneORing {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

FirstOrder.Structure.Monotone ℒₒᵣ M

source

@[simp]

theorem LO.Arith.zero_ne_add_one {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

0 ≠ x + 1

source

@[simp]

theorem LO.Arith.nat_cast_inj {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {n m : ℕ} :

↑n = ↑m ↔ n = m

source

@[simp]

theorem LO.Arith.coe_coe_lt {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {n m : ℕ} :

↑n < ↑m ↔ n < m

source

theorem LO.Arith.coe_succ {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : ℕ) :

↑(x + 1) = ↑x + 1

TODO: move

source

@[reducible, inline]

abbrev LO.Arith.natCast (M : Type u_1) [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

NatCast M

Equations

LO.Arith.natCast M = inferInstance

source

@[simp]

theorem LO.Arith.natCast_nat (n : ℕ) :

↑n = n

source

@[simp]

theorem LO.FirstOrder.Semiformula.eval_ballLTSucc' {M : Type u_1} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻] {L : Language} [L.LT] [L.Zero] [L.One] [L.Add] [Structure L M] [Structure.LT L M] [Structure.One L M] [Structure.Add L M] {ξ : Type u_2} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} :

(Evalm M e ε) (ballLTSucc t φ) ↔ ∀ x ≤ Semiterm.valm M e ε t, (Evalm M (x :> e) ε) φ

source

@[simp]

theorem LO.FirstOrder.Semiformula.eval_bexLTSucc' {M : Type u_1} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻] {L : Language} [L.LT] [L.Zero] [L.One] [L.Add] [Structure L M] [Structure.LT L M] [Structure.One L M] [Structure.Add L M] {ξ : Type u_2} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} :

(Evalm M e ε) (bexLTSucc t φ) ↔ ∃ x ≤ Semiterm.valm M e ε t, (Evalm M (x :> e) ε) φ