MathematicalLogic.SecondOrder.Theories.Real

source

def SecondOrder.Language.orderedRing :

Language

Equations

SecondOrder.Language.orderedRing = { Func := SecondOrder.Language.orderedRing.Func✝, Rel := SecondOrder.Language.orderedRing.Rel✝ }

Instances For

source

instance SecondOrder.Language.orderedRing.instZeroTerm {l : List Ty} :

Zero (orderedRing.Term l)

Equations

SecondOrder.Language.orderedRing.instZeroTerm = { zero := SecondOrder.Language.orderedRing.Func.zero✝ ⬝ᶠ []ᵥ }

source

instance SecondOrder.Language.orderedRing.instOneTerm {l : List Ty} :

One (orderedRing.Term l)

Equations

SecondOrder.Language.orderedRing.instOneTerm = { one := SecondOrder.Language.orderedRing.Func.one✝ ⬝ᶠ []ᵥ }

source

instance SecondOrder.Language.orderedRing.instAddTerm {l : List Ty} :

Add (orderedRing.Term l)

Equations

SecondOrder.Language.orderedRing.instAddTerm = { add := fun (x1 x2 : SecondOrder.Language.orderedRing.Term l) => SecondOrder.Language.orderedRing.Func.add✝ ⬝ᶠ [x1, x2]ᵥ }

source

instance SecondOrder.Language.orderedRing.instNegTerm {l : List Ty} :

Neg (orderedRing.Term l)

Equations

SecondOrder.Language.orderedRing.instNegTerm = { neg := fun (x : SecondOrder.Language.orderedRing.Term l) => SecondOrder.Language.orderedRing.Func.neg✝ ⬝ᶠ [x]ᵥ }

source

instance SecondOrder.Language.orderedRing.instMulTerm {l : List Ty} :

Mul (orderedRing.Term l)

Equations

SecondOrder.Language.orderedRing.instMulTerm = { mul := fun (x1 x2 : SecondOrder.Language.orderedRing.Term l) => SecondOrder.Language.orderedRing.Func.mul✝ ⬝ᶠ [x1, x2]ᵥ }

source

def SecondOrder.Language.orderedRing.le {l : List Ty} (t₁ t₂ : orderedRing.Term l) :

orderedRing.Formula l

Equations

SecondOrder.Language.orderedRing.le t₁ t₂ = SecondOrder.Language.orderedRing.Rel.le✝ ⬝ʳ [t₁, t₂]ᵥ

Instances For

source

def SecondOrder.Language.orderedRing.«term_⪯_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance SecondOrder.Language.orderedRing.Real :

orderedRing.HasStructure ℝ

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem SecondOrder.Language.orderedRing.Real.interp_zero {l : List Ty} {ρ : Assignment ℝ l} :

⟦ 0 ⟧ₜ ℝ , ρ = 0

source

@[simp]

theorem SecondOrder.Language.orderedRing.Real.interp_one {l : List Ty} {ρ : Assignment ℝ l} :

⟦ 1 ⟧ₜ ℝ , ρ = 1

source

@[simp]

theorem SecondOrder.Language.orderedRing.Real.interp_add {l : List Ty} {t₁ t₂ : orderedRing.Term l} {ρ : Assignment ℝ l} :

⟦ t₁ + t₂ ⟧ₜ ℝ , ρ = (⟦ t₁ ⟧ₜ ℝ , ρ) + (⟦ t₂ ⟧ₜ ℝ , ρ)

source

@[simp]

theorem SecondOrder.Language.orderedRing.Real.interp_neg {l : List Ty} {t : orderedRing.Term l} {ρ : Assignment ℝ l} :

⟦ -t ⟧ₜ ℝ , ρ = -(⟦ t ⟧ₜ ℝ , ρ)

source

@[simp]

theorem SecondOrder.Language.orderedRing.Real.interp_mul {l : List Ty} {t₁ t₂ : orderedRing.Term l} {ρ : Assignment ℝ l} :

⟦ t₁ * t₂ ⟧ₜ ℝ , ρ = (⟦ t₁ ⟧ₜ ℝ , ρ) * (⟦ t₂ ⟧ₜ ℝ , ρ)

source

@[simp]

theorem SecondOrder.Language.orderedRing.Real.satisfy_le {l : List Ty} {t₁ t₂ : orderedRing.Term l} {ρ : Assignment ℝ l} :

ℝ ⊨[ρ] le t₁ t₂ ↔ ⟦ t₁ ⟧ₜ ℝ , ρ ≤ ⟦ t₂ ⟧ₜ ℝ , ρ

source

inductive SecondOrder.Language.Theory.Real :

orderedRing.Theory

ax_add_assoc : Real (∀' ∀' ∀' (#2 + #1 + #0 ≐ #2 + (#1 + #0)))
ax_add_comm : Real (∀' ∀' (#1 + #0 ≐ #0 + #1))
ax_add_zero : Real (∀' (#0 + 0 ≐ #0))
ax_add_neg : Real (∀' (#0 + -#0 ≐ 0))
ax_mul_assoc : Real (∀' ∀' ∀' (#2 * #1 * #0 ≐ #2 * (#1 * #0)))
ax_mul_comm : Real (∀' ∀' (#1 * #0 ≐ #0 * #1))
ax_mul_one : Real (∀' (#0 * 1 ≐ #0))
ax_has_inv : Real (∀' (~ #0 ≐ 0 ⇒ ∃' (#1 * #0 ≐ 1)))
ax_left_distrib : Real (∀' ∀' ∀' (#2 * (#1 + #0) ≐ #2 * #1 + #2 * #0))
ax_zero_ne_one : Real (~ 0 ≐ 1)
ax_le_refl : Real (∀' orderedRing.le #0 #0)
ax_le_antisymm : Real (∀' ∀' (orderedRing.le #1 #0 ⇒ orderedRing.le #0 #1 ⇒ #1 ≐ #0))
ax_le_trans : Real (∀' ∀' ∀' (orderedRing.le #2 #1 ⇒ orderedRing.le #1 #0 ⇒ orderedRing.le #2 #0))
ax_le_total : Real (∀' ∀' (orderedRing.le #1 #0 ⩒ orderedRing.le #0 #1))
ax_add_le_add : Real (∀' ∀' ∀' (orderedRing.le #2 #1 ⇒ orderedRing.le (#2 + #0) (#1 + #0)))
ax_mul_le_mul : Real (∀' ∀' ∀' (orderedRing.le #2 #1 ⇒ orderedRing.le 0 #0 ⇒ orderedRing.le (#2 * #0) (#1 * #0)))
ax_exists_lub : Real (∀ʳ[1](∃' (1 ⬝ʳᵛ [#0]ᵥ) ⇒ ∃' ∀' (2 ⬝ʳᵛ [#0]ᵥ ⇒ orderedRing.le #0 #1) ⇒ ∃' (∀' (2 ⬝ʳᵛ [#0]ᵥ ⇒ orderedRing.le #0 #1) ⩑ ∀' (∀' (3 ⬝ʳᵛ [#0]ᵥ ⇒ orderedRing.le #0 #1) ⇒ orderedRing.le #1 #0))))

Instances For

source

instance SecondOrder.Language.Theory.Real.instIsModelReal :

Real.IsModel ℝ

source

instance SecondOrder.Language.Theory.Real.instZeroDom {M : Real.Model} :

Zero M.Dom

Equations

SecondOrder.Language.Theory.Real.instZeroDom = { zero := M.interpFunc SecondOrder.Language.orderedRing.Func.zero✝ []ᵥ }

source

instance SecondOrder.Language.Theory.Real.instOneDom {M : Real.Model} :

One M.Dom

Equations

SecondOrder.Language.Theory.Real.instOneDom = { one := M.interpFunc SecondOrder.Language.orderedRing.Func.one✝ []ᵥ }

source

instance SecondOrder.Language.Theory.Real.instAddDom {M : Real.Model} :

Add M.Dom

Equations

SecondOrder.Language.Theory.Real.instAddDom = { add := fun (x1 x2 : M.Dom) => M.interpFunc SecondOrder.Language.orderedRing.Func.add✝ [x1, x2]ᵥ }

source

instance SecondOrder.Language.Theory.Real.instNegDom {M : Real.Model} :

Neg M.Dom

Equations

SecondOrder.Language.Theory.Real.instNegDom = { neg := fun (x : M.Dom) => M.interpFunc SecondOrder.Language.orderedRing.Func.neg✝ [x]ᵥ }

source

instance SecondOrder.Language.Theory.Real.instMulDom {M : Real.Model} :

Mul M.Dom

Equations

SecondOrder.Language.Theory.Real.instMulDom = { mul := fun (x1 x2 : M.Dom) => M.interpFunc SecondOrder.Language.orderedRing.Func.mul✝ [x1, x2]ᵥ }

source

instance SecondOrder.Language.Theory.Real.instLEDom {M : Real.Model} :

LE M.Dom

Equations

SecondOrder.Language.Theory.Real.instLEDom = { le := fun (x1 x2 : M.Dom) => M.interpRel SecondOrder.Language.orderedRing.Rel.le✝ [x1, x2]ᵥ }

source

@[simp]

theorem SecondOrder.Language.Theory.Real.interp_zero {l : List Ty} {M : Real.Model} {ρ : Assignment M.Dom l} :

⟦ 0 ⟧ₜ M.Dom, ρ = 0

source

@[simp]

theorem SecondOrder.Language.Theory.Real.interp_one {l : List Ty} {M : Real.Model} {ρ : Assignment M.Dom l} :

⟦ 1 ⟧ₜ M.Dom, ρ = 1

source

@[simp]

theorem SecondOrder.Language.Theory.Real.interp_add {l : List Ty} {M : Real.Model} {t₁ t₂ : orderedRing.Term l} {ρ : Assignment M.Dom l} :

⟦ t₁ + t₂ ⟧ₜ M.Dom, ρ = (⟦ t₁ ⟧ₜ M.Dom, ρ) + (⟦ t₂ ⟧ₜ M.Dom, ρ)

source

@[simp]

theorem SecondOrder.Language.Theory.Real.interp_neg {l : List Ty} {M : Real.Model} {t : orderedRing.Term l} {ρ : Assignment M.Dom l} :

⟦ -t ⟧ₜ M.Dom, ρ = -(⟦ t ⟧ₜ M.Dom, ρ)

source

@[simp]

theorem SecondOrder.Language.Theory.Real.interp_mul {l : List Ty} {M : Real.Model} {t₁ t₂ : orderedRing.Term l} {ρ : Assignment M.Dom l} :

⟦ t₁ * t₂ ⟧ₜ M.Dom, ρ = (⟦ t₁ ⟧ₜ M.Dom, ρ) * (⟦ t₂ ⟧ₜ M.Dom, ρ)

source

@[simp]

theorem SecondOrder.Language.Theory.Real.satisfy_le {l : List Ty} {M : Real.Model} {t₁ t₂ : orderedRing.Term l} {ρ : Assignment M.Dom l} :

M.Dom ⊨[ρ] orderedRing.le t₁ t₂ ↔ ⟦ t₁ ⟧ₜ M.Dom, ρ ≤ ⟦ t₂ ⟧ₜ M.Dom, ρ

source

theorem SecondOrder.Language.Theory.Real.add_comm {M : Real.Model} (a b : M.Dom) :

a + b = b + a

source

theorem SecondOrder.Language.Theory.Real.add_zero {M : Real.Model} (a : M.Dom) :

a + 0 = a

source

instance SecondOrder.Language.Theory.Real.instAddCommGroupDom {M : Real.Model} :

AddCommGroup M.Dom

Equations

One or more equations did not get rendered due to their size.

source

theorem SecondOrder.Language.Theory.Real.mul_comm {M : Real.Model} (a b : M.Dom) :

a * b = b * a

source

theorem SecondOrder.Language.Theory.Real.mul_one {M : Real.Model} (a : M.Dom) :

a * 1 = a

source

theorem SecondOrder.Language.Theory.Real.left_distrib {M : Real.Model} (a b c : M.Dom) :

a * (b + c) = a * b + a * c

source

theorem SecondOrder.Language.Theory.Real.mul_zero {M : Real.Model} (a : M.Dom) :

a * 0 = 0

source

theorem SecondOrder.Language.Theory.Real.has_inv {M : Real.Model} (a : M.Dom) :

a ≠ 0 → ∃ (b : M.Dom), a * b = 1

source

noncomputable instance SecondOrder.Language.Theory.Real.instInvDom {M : Real.Model} :

Inv M.Dom

Equations

SecondOrder.Language.Theory.Real.instInvDom = { inv := fun (a : M.Dom) => if h : a = 0 then 0 else Classical.choose ⋯ }

source

noncomputable instance SecondOrder.Language.Theory.Real.instFieldDom {M : Real.Model} :

Field M.Dom

Equations

One or more equations did not get rendered due to their size.

source

noncomputable instance SecondOrder.Language.Theory.Real.instLinearOrderDom {M : Real.Model} :

LinearOrder M.Dom

Equations

One or more equations did not get rendered due to their size.

source

theorem SecondOrder.Language.Theory.Real.add_le_add_right {M : Real.Model} (a b c : M.Dom) :

a ≤ b → a + c ≤ b + c

source

theorem SecondOrder.Language.Theory.Real.zero_le_neg_iff {M : Real.Model} (a : M.Dom) :

0 ≤ -a ↔ a ≤ 0

source

theorem SecondOrder.Language.Theory.Real.mul_le_mul_right {M : Real.Model} (a b c : M.Dom) :

a ≤ b → 0 ≤ c → a * c ≤ b * c

source

instance SecondOrder.Language.Theory.Real.instIsStrictOrderedRingDom {M : Real.Model} :

IsStrictOrderedRing M.Dom

source

theorem SecondOrder.Language.Theory.Real.exists_lub {M : Real.Model} (s : Set M.Dom) :

s.Nonempty → BddAbove s → ∃ (u : M.Dom), IsLUB s u

source

noncomputable def SecondOrder.Language.Theory.Real.ofReal {M : Real.Model} (x : ℝ) :

M.Dom

Equations

SecondOrder.Language.Theory.Real.ofReal x = Classical.choose ⋯

Instances For

source

theorem SecondOrder.Language.Theory.Real.ofReal_isLUB {M : Real.Model} {x : ℝ} :

IsLUB {x_1 : M.Dom | ∃ (y : ℚ) (_ : ↑y ≤ x), ↑y = x_1} (ofReal x)

source

theorem SecondOrder.Language.Theory.Real.ofReal_rat {M : Real.Model} {q : ℚ} :

ofReal ↑q = ↑q

source

theorem SecondOrder.Language.Theory.Real.ofReal_zero {M : Real.Model} :

ofReal 0 = 0

source

theorem SecondOrder.Language.Theory.Real.ofReal_one {M : Real.Model} :

ofReal 1 = 1

source

theorem SecondOrder.Language.Theory.Real.ofReal_lt {M : Real.Model} {x y : ℝ} :

ofReal x < ofReal y ↔ x < y

source

theorem SecondOrder.Language.Theory.Real.ofReal_le {M : Real.Model} {x y : ℝ} :

ofReal x ≤ ofReal y ↔ x ≤ y

source

theorem SecondOrder.Language.Theory.Real.ofReal_injective {M : Real.Model} :

Function.Injective ofReal

source

theorem SecondOrder.Language.Theory.Real.exists_nat_gt {M : Real.Model} (a : M.Dom) :

∃ (n : ℕ), a < ↑n

source

instance SecondOrder.Language.Theory.Real.instArchimedeanDom {M : Real.Model} :

Archimedean M.Dom

source

theorem SecondOrder.Language.Theory.Real.ofReal_surjective {M : Real.Model} :

Function.Surjective ofReal

source

theorem SecondOrder.Language.Theory.Real.ofReal_add {M : Real.Model} {x y : ℝ} :

ofReal (x + y) = ofReal x + ofReal y

source

theorem SecondOrder.Language.Theory.Real.ofReal_neg {M : Real.Model} {x : ℝ} :

ofReal (-x) = -ofReal x

source

theorem SecondOrder.Language.Theory.Real.exists_sqrt {M : Real.Model} (a : M.Dom) (h : 0 ≤ a) :

∃ (b : M.Dom), 0 ≤ b ∧ b ^ 2 = a

source

theorem SecondOrder.Language.Theory.Real.ofReal_mul {M : Real.Model} {x y : ℝ} :

ofReal (x * y) = ofReal x * ofReal y

source

theorem SecondOrder.Language.Theory.Real.ofReal_inv {M : Real.Model} {x : ℝ} :

ofReal x⁻¹ = (ofReal x)⁻¹

source

theorem SecondOrder.Language.Theory.Real.iso_Real (M : Real.Model) :

Nonempty (M.toStructure ≃ᴹ Structure.of ℝ)

source

theorem SecondOrder.Language.Theory.Real.categorical :

Real.Categorical