Theory $\mathsf{I}\Sigma_0 + \Omega_1$ #

source

def LO.Omega1.omega1 :

FirstOrder.SyntacticFormula ℒₒᵣ

∀ x, ∃ y, 2^{|x|^2} = y

Equations

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

Instances For

source

inductive LO.Omega1 :

FirstOrder.Theory ℒₒᵣ

omega : 𝛀₁ omega1

Instances For

source

def LO.Omega1.«term𝛀₁» :

Lean.ParserDescr

Equations

LO.Omega1.«term𝛀₁» = Lean.ParserDescr.node `LO.Omega1.«term𝛀₁» 1024 (Lean.ParserDescr.symbol "𝛀₁")

Instances For

source

@[simp]

theorem LO.FirstOrder.Theory.OmegaOne.mem_iff {σ : SyntacticFormula ℒₒᵣ} :

σ ∈ 𝛀₁ ↔ σ = Omega1.omega1

source

theorem LO.Omega1.models_Omega1_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

V ⊧ₘ omega1 ↔ ∀ (x : V), ∃ (y : V), ISigma0.Exponential (‖x‖ ^ 2) y

source

theorem LO.Omega1.omega1_of_ISigma1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

V ⊧ₘ omega1

source

instance LO.Omega1.instModelsTheoryHAddArithmeticTheoryTheoryORingISigmaOfNatNat {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁

source

instance LO.Omega1.instModelsTheoryISigmaOfNatNat {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] :

V ⊧ₘ* 𝐈𝚺₀

source

instance LO.Omega1.instModelsTheory {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] :

V ⊧ₘ* 𝛀₁

source

theorem LO.Omega1.exists_exponential_sq_length {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (x : V) :

∃ (y : V), ISigma0.Exponential (‖x‖ ^ 2) y

source

theorem LO.Omega1.exists_unique_exponential_sq_length {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (x : V) :

∃! y : V, ISigma0.Exponential (‖x‖ ^ 2) y

source

theorem LO.Omega1.smash_exists_unique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (x y : V) :

∃! z : V, ISigma0.Exponential (‖x‖ * ‖y‖) z

source

instance LO.Omega1.instSmash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] :

Smash V

Equations

LO.Omega1.instSmash = { smash := fun (a b : V) => Classical.choose! ⋯ }

source

theorem LO.Omega1.exponential_smash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) :

ISigma0.Exponential (‖a‖ * ‖b‖) (a ⨳ b)

source

theorem LO.Omega1.exponential_smash_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) :

ISigma0.Exponential ‖a‖ (a ⨳ 1)

source

def LO.Omega1.smashDef :

𝚺₀.Semisentence 3

Equations

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

Instances For

source

theorem LO.Omega1.smash_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] :

𝚺₀ -Function₂ Smash.smash via smashDef

source

instance LO.Omega1.smash_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] :

𝚺₀ -Function₂ Smash.smash

source

@[simp]

theorem LO.Omega1.smash_pow2 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) :

ISigma0.Pow2 (a ⨳ b)

source

@[simp]

theorem LO.Omega1.smash_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) :

0 < a ⨳ b

source

@[simp]

theorem LO.Omega1.smash_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) :

‖a‖ * ‖b‖ < a ⨳ b

source

theorem LO.Omega1.length_smash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) :

‖a ⨳ b‖ = ‖a‖ * ‖b‖ + 1

source

@[simp]

theorem LO.Omega1.smash_zero_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) :

0 ⨳ a = 1

source

@[simp]

theorem LO.Omega1.smash_zero_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) :

a ⨳ 0 = 1

source

theorem LO.Omega1.smash_comm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) :

a ⨳ b = b ⨳ a

source

@[simp]

theorem LO.Omega1.lt_smash_one_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) :

a < a ⨳ 1

source

@[simp]

theorem LO.Omega1.lt_smash_one_righs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) :

a ⨳ 1 ≤ 2 * a + 1

source

theorem LO.Omega1.lt_smash_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a b c : V} :

a < b ⨳ c ↔ ‖a‖ ≤ ‖b‖ * ‖c‖

source

theorem LO.Omega1.smash_le_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a b c : V} :

b ⨳ c ≤ a ↔ ‖b‖ * ‖c‖ < ‖a‖

source

theorem LO.Omega1.lt_smash_one_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a b : V} :

a < b ⨳ 1 ↔ ‖a‖ ≤ ‖b‖

source

theorem LO.Omega1.smash_monotone {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a₁ a₂ b₁ b₂ : V} (h₁ : a₁ ≤ b₁) (h₂ : a₂ ≤ b₂) :

a₁ ⨳ a₂ ≤ b₁ ⨳ b₂

source

theorem LO.Omega1.bexp_eq_smash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) :

ISigma0.bexp (a ⨳ b) (‖a‖ * ‖b‖) = a ⨳ b

source

theorem LO.Omega1.smash_two_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) {b : V} (pos : 0 < b) :

a ⨳ (2 * b) = a ⨳ b * a ⨳ 1

source

theorem LO.Omega1.smash_two_mul_le_sq_smash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) :

a ⨳ (2 * b) ≤ (a ⨳ b) ^ 2

source

instance LO.Omega1.instWeakerThanSyntacticFormulaORingArithmeticTheoryISigmaOfNatNatHAddTheory :

𝐈𝚺₀ ⪯ 𝐈𝚺₀ + 𝛀₁

source

instance LO.Omega1.instWeakerThanSyntacticFormulaORingArithmeticTheoryHAddTheoryISigmaOfNatNat :

𝐈𝚺₀ + 𝛀₁ ⪯ 𝐈𝚺₁

source

instance LO.Omega1.instModelsTheoryNatHAddArithmeticTheoryTheoryORingISigmaOfNat :

ℕ ⊧ₘ* 𝐈𝚺₀ + 𝛀₁

Documentation

Foundation.FirstOrder.Omega1.Basic

Theory $\mathsf{I}\Sigma_0 + \Omega_1$ #