class
LO.FirstOrder.Structure.Monotone
(L : LO.FirstOrder.Language)
(M : Type u_1)
[LE M]
[LO.FirstOrder.Structure L M]
:
- monotone : ∀ {k : ℕ} (f : L.Func k) (v₁ v₂ : Fin k → M), (∀ (i : Fin k), v₁ i ≤ v₂ i) → LO.FirstOrder.Structure.func f v₁ ≤ LO.FirstOrder.Structure.func f v₂
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 k → M)
(v₂ : Fin k → M)
:
(∀ (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 n → M}
{e₂ : Fin n → M}
{ε₁ : ξ → M}
{ε₂ : ξ → M}
(he : ∀ (i : Fin n), e₁ i ≤ e₂ i)
(hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i)
:
LO.FirstOrder.Semiterm.valm M e₁ ε₁ t ≤ LO.FirstOrder.Semiterm.valm M e₂ ε₂ t
def
LO.FirstOrder.Semiterm.arithCases
{ξ : Type u_1}
{n : ℕ}
{C : LO.FirstOrder.Semiterm ℒₒᵣ ξ n → Sort 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 ℒₒᵣ ξ n → Sort 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 → C u → C (‘(!!t + !!u)’))
(hmul : {t u : LO.FirstOrder.Semiterm ℒₒᵣ ξ n} → C t → C u → C (‘(!!t * !!u)’))
(t : LO.FirstOrder.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)
Instances For
Equations
- ⋯ = ⋯
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
LO.Arith.le_mul_of_pos_right
{M : Type u_1}
[LO.ORingStruc M]
[M ⊧ₘ* 𝐏𝐀⁻]
{a : M}
{b : M}
(h : 0 < b)
:
theorem
LO.Arith.le_mul_of_pos_left
{M : Type u_1}
[LO.ORingStruc M]
[M ⊧ₘ* 𝐏𝐀⁻]
{a : M}
{b : M}
(h : 0 < b)
:
@[simp]
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)
:
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)
:
theorem
LO.Arith.mul_le_mul_left
{M : Type u_1}
[LO.ORingStruc M]
[M ⊧ₘ* 𝐏𝐀⁻]
{a : M}
{b : M}
{c : M}
(h : b ≤ 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)
:
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
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]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
LO.Arith.lt_square_of_lt
{M : Type u_1}
[LO.ORingStruc M]
[M ⊧ₘ* 𝐏𝐀⁻]
{a : M}
(pos : 1 < a)
:
theorem
LO.Arith.succ_le_double_of_pos
{M : Type u_1}
[LO.ORingStruc M]
[M ⊧ₘ* 𝐏𝐀⁻]
{a : M}
(h : 0 < a)
:
@[simp]
theorem
LO.Arith.le_add_add_left
{M : Type u_1}
[LO.ORingStruc M]
[M ⊧ₘ* 𝐏𝐀⁻]
(a : M)
(b : M)
(c : M)
:
@[simp]
theorem
LO.Arith.le_add_add_right
{M : Type u_1}
[LO.ORingStruc M]
[M ⊧ₘ* 𝐏𝐀⁻]
(a : M)
(b : M)
(c : M)
:
@[simp]
theorem
LO.Arith.val_npow
{M : Type u_1}
[LO.ORingStruc M]
[M ⊧ₘ* 𝐏𝐀⁻]
(k : ℕ)
(a : M)
:
(LO.FirstOrder.Semiterm.Operator.npow ℒₒᵣ k).val ![a] = a ^ k
Equations
- LO.Arith.instMonotoneORing = { monotone := ⋯ }
@[simp]
TODO: move
@[simp]
theorem
LO.FirstOrder.Semiformula.eval_ballLTSucc'
{M : Type u_1}
[Zero M]
[One M]
[Add M]
[Mul M]
[LT M]
[M ⊧ₘ* 𝐏𝐀⁻]
{L : LO.FirstOrder.Language}
[L.LT]
[L.Zero]
[L.One]
[L.Add]
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.LT L M]
[LO.FirstOrder.Structure.One L M]
[LO.FirstOrder.Structure.Add L M]
{ξ : Type u_2}
{n : ℕ}
{e : Fin n → M}
{ε : ξ → M}
{t : LO.FirstOrder.Semiterm L ξ n}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
:
(LO.FirstOrder.Semiformula.Evalm M e ε) (LO.FirstOrder.Semiformula.ballLTSucc t p) ↔ ∀ x ≤ LO.FirstOrder.Semiterm.valm M e ε t, (LO.FirstOrder.Semiformula.Evalm M (x :> e) ε) p
@[simp]
theorem
LO.FirstOrder.Semiformula.eval_bexLTSucc'
{M : Type u_1}
[Zero M]
[One M]
[Add M]
[Mul M]
[LT M]
[M ⊧ₘ* 𝐏𝐀⁻]
{L : LO.FirstOrder.Language}
[L.LT]
[L.Zero]
[L.One]
[L.Add]
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.LT L M]
[LO.FirstOrder.Structure.One L M]
[LO.FirstOrder.Structure.Add L M]
{ξ : Type u_2}
{n : ℕ}
{e : Fin n → M}
{ε : ξ → M}
{t : LO.FirstOrder.Semiterm L ξ n}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
:
(LO.FirstOrder.Semiformula.Evalm M e ε) (LO.FirstOrder.Semiformula.bexLTSucc t p) ↔ ∃ x ≤ LO.FirstOrder.Semiterm.valm M e ε t, (LO.FirstOrder.Semiformula.Evalm M (x :> e) ε) p