instance instNonemptyOfZero_arithmetization {α : Type u_1} [Zero α] : Nonempty α

Equations

• ⋯ = ⋯

def termExp_ : Lean.ParserDescr

Equations

• termExp_ = Lean.ParserDescr.node `termExp_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "exp ") (Lean.ParserDescr.cat `term 90))

theorem Matrix.forall_iff {α : Type u_1} {n : ℕ} (p : (Fin (n + 1) → α) → Prop) : (∀ (v : Fin (n + 1) → α), p v) ↔ ∀ (a : α) (v : Fin n → α), p (a :> v)

theorem Matrix.comp_vecCons₂' {β : Sort u_1} {γ : Type u_2} {α : Type u_3} {n : ℕ} (g : β → γ) (f : α → β) (a : α) (s : Fin n → α) : (fun (x : Fin n.succ) => g (f ((a :> s) x))) = g (f a) :> fun (i : Fin n) => g (f (s i))

@[simp]

theorem Set.subset_union_three₁ {α : Type u_1} (s : Set α) (t : Set α) (u : Set α) : s ⊆ s ∪ t ∪ u

@[simp]

theorem Set.subset_union_three₂ {α : Type u_1} (s : Set α) (t : Set α) (u : Set α) : t ⊆ s ∪ t ∪ u

@[simp]

theorem Set.subset_union_three₃ {α : Type u_1} (s : Set α) (t : Set α) (u : Set α) : u ⊆ s ∪ t ∪ u

theorem Matrix.fun_eq_vec₃ {α : Type u_1} {v : Fin 3 → α} : v = ![v 0, v 1, v 2]

theorem Matrix.fun_eq_vec₄ {α : Type u_1} {v : Fin 4 → α} : v = ![v 0, v 1, v 2, v 3]

@[simp]

theorem Matrix.cons_app_four {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ → α) : (a :> s) 4 = s 3

@[simp]

theorem Matrix.cons_app_five {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ → α) : (a :> s) 5 = s 4

@[simp]

theorem Matrix.cons_app_six {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ → α) : (a :> s) 6 = s 5

@[simp]

theorem Matrix.cons_app_seven {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 7 = s 6

@[simp]

theorem Matrix.cons_app_eight {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 8 = s 7

theorem Matrix.eq_vecCons' {n : ℕ} {C : Type u_1} (s : Fin (n + 1) → C) : (s 0 :> fun (x : Fin n) => s x.succ) = s

theorem forall_fin_iff_zero_and_forall_succ {k : ℕ} {P : Fin (k + 1) → Prop} : (∀ (i : Fin (k + 1)), P i) ↔ P 0 ∧ ∀ (i : Fin k), P i.succ

theorem exists_fin_iff_zero_or_exists_succ {k : ℕ} {P : Fin (k + 1) → Prop} : (∃ (i : Fin (k + 1)), P i) ↔ P 0 ∨ ∃ (i : Fin k), P i.succ

theorem forall_vec_iff_forall_forall_vec {k : ℕ} {α : Type u_1} {P : (Fin (k + 1) → α) → Prop} : (∀ (v : Fin (k + 1) → α), P v) ↔ ∀ (x : α) (v : Fin k → α), P (x :> v)

theorem exists_vec_iff_exists_exists_vec {k : ℕ} {α : Type u_1} {P : (Fin (k + 1) → α) → Prop} : (∃ (v : Fin (k + 1) → α), P v) ↔ ∃ (x : α) (v : Fin k → α), P (x :> v)

theorem exists_le_vec_iff_exists_le_exists_vec {α : Type u_1} {k : ℕ} [LE α] {P : (Fin (k + 1) → α) → Prop} {f : Fin (k + 1) → α} : (∃ v ≤ f, P v) ↔ ∃ x ≤ f 0, ∃ v ≤ fun (x : Fin k) => f x.succ, P (x :> v)

theorem forall_le_vec_iff_forall_le_forall_vec {α : Type u_1} {k : ℕ} [LE α] {P : (Fin (k + 1) → α) → Prop} {f : Fin (k + 1) → α} : (∀ v ≤ f, P v) ↔ ∀ x ≤ f 0, ∀ v ≤ fun (x : Fin k) => f x.succ, P (x :> v)

instance instToStringEmpty_arithmetization : ToString Empty

Equations

• instToStringEmpty_arithmetization = { toString := Empty.elim }

class Hash (α : Type u_1) : Type u_1

• hash : α → α → α

Instances

• LO.Arith.instHash

def «term_#_» : Lean.TrailingParserDescr

Equations

• «term_#_» = Lean.ParserDescr.trailingNode `term_#_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " # ") (Lean.ParserDescr.cat `term 81))

class Length (α : Type u_1) : Type u_1

• length : α → α

def «term‖_‖» : Lean.ParserDescr

Equations

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

def LO.Polarity.coe {α : Type u_1} [LO.SigmaSymbol α] [LO.PiSymbol α] : LO.Polarity → α

Equations

• x.coe = match x with | LO.Polarity.sigma => 𝚺 | LO.Polarity.pi => 𝚷

instance LO.Polarity.instCoe_arithmetization {α : Type u_1} [LO.SigmaSymbol α] [LO.PiSymbol α] : Coe LO.Polarity α

Equations

• LO.Polarity.instCoe_arithmetization = { coe := LO.Polarity.coe }

@[simp]

theorem LO.Polarity.coe_sigma {α : Type u_1} [LO.SigmaSymbol α] [LO.PiSymbol α] : 𝚺.coe = 𝚺

@[simp]

theorem LO.Polarity.coe_pi {α : Type u_1} [LO.SigmaSymbol α] [LO.PiSymbol α] : 𝚷.coe = 𝚷

@[simp]

theorem LO.SigmaPiDelta.alt_coe (Γ : LO.Polarity) : Γ.coe.alt = Γ.alt.coe

def LO.FirstOrder.Arith.termToStr {μ : Type u_1} [ToString μ] {n : ℕ} : LO.FirstOrder.Semiterm ℒₒᵣ μ n → String

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.bvar x_1) = "x_{" ++ toString (n - 1 - ↑x_1) ++ "}"
• LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.fvar x_1) = "a_{" ++ toString x_1 ++ "}"
• LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.zero a) = "0"
• LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.one a) = "1"

instance LO.FirstOrder.Arith.instReprSemitermORing_arithmetization {μ : Type u_1} [ToString μ] {n : ℕ} : Repr (LO.FirstOrder.Semiterm ℒₒᵣ μ n)

Equations

• LO.FirstOrder.Arith.instReprSemitermORing_arithmetization = { reprPrec := fun (t : LO.FirstOrder.Semiterm ℒₒᵣ μ n) (x : ℕ) => Std.Format.text (LO.FirstOrder.Arith.termToStr t) }

instance LO.FirstOrder.Arith.instToStringSemitermORing_arithmetization {μ : Type u_1} [ToString μ] {n : ℕ} : ToString (LO.FirstOrder.Semiterm ℒₒᵣ μ n)

Equations

• LO.FirstOrder.Arith.instToStringSemitermORing_arithmetization = { toString := LO.FirstOrder.Arith.termToStr }

def LO.FirstOrder.Arith.formulaToStr {μ : Type u_1} [ToString μ] {n : ℕ} : LO.FirstOrder.Semiformula ℒₒᵣ μ n → String

instance LO.FirstOrder.Arith.instReprSemiformulaORing_arithmetization {μ : Type u_1} [ToString μ] {n : ℕ} : Repr (LO.FirstOrder.Semiformula ℒₒᵣ μ n)

Equations

• LO.FirstOrder.Arith.instReprSemiformulaORing_arithmetization = { reprPrec := fun (t : LO.FirstOrder.Semiformula ℒₒᵣ μ n) (x : ℕ) => Std.Format.text (LO.FirstOrder.Arith.formulaToStr t) }

instance LO.FirstOrder.Arith.instToStringSemiformulaORing_arithmetization {μ : Type u_1} [ToString μ] {n : ℕ} : ToString (LO.FirstOrder.Semiformula ℒₒᵣ μ n)

Equations

• LO.FirstOrder.Arith.instToStringSemiformulaORing_arithmetization = { toString := LO.FirstOrder.Arith.formulaToStr }

instance LO.FirstOrder.Arith.indScheme_of_indH (M : Type u_1) [LO.ORingStruc M] (Γ : LO.Polarity) (n : ℕ) [M ⊧ₘ* 𝐈𝐍𝐃Γ n] : M ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ n)

Equations

• ⋯ = ⋯

@[simp]

theorem LO.FirstOrder.Semiformula.eval_operator₃ {ξ : Type u_3} {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} {n : ℕ} {ε : ξ → M} {e : Fin n → M} {o : LO.FirstOrder.Semiformula.Operator L 3} {t₁ : LO.FirstOrder.Semiterm L ξ n} {t₂ : LO.FirstOrder.Semiterm L ξ n} {t₃ : LO.FirstOrder.Semiterm L ξ n} : (LO.FirstOrder.Semiformula.Eval s e ε) (o.operator ![t₁, t₂, t₃]) ↔ o.val ![LO.FirstOrder.Semiterm.val s e ε t₁, LO.FirstOrder.Semiterm.val s e ε t₂, LO.FirstOrder.Semiterm.val s e ε t₃]

@[simp]

theorem LO.FirstOrder.Semiformula.eval_operator₄ {ξ : Type u_3} {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} {n : ℕ} {ε : ξ → M} {e : Fin n → M} {o : LO.FirstOrder.Semiformula.Operator L 4} {t₁ : LO.FirstOrder.Semiterm L ξ n} {t₂ : LO.FirstOrder.Semiterm L ξ n} {t₃ : LO.FirstOrder.Semiterm L ξ n} {t₄ : LO.FirstOrder.Semiterm L ξ n} : (LO.FirstOrder.Semiformula.Eval s e ε) (o.operator ![t₁, t₂, t₃, t₄]) ↔ o.val ![LO.FirstOrder.Semiterm.val s e ε t₁, LO.FirstOrder.Semiterm.val s e ε t₂, LO.FirstOrder.Semiterm.val s e ε t₃, LO.FirstOrder.Semiterm.val s e ε t₄]

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.Rlz {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] {n : ℕ} (t : LO.FirstOrder.Semiterm L M n) (e : Fin n → M) : M

Equations

• t.Rlz e = LO.FirstOrder.Semiterm.valm M e id t

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Rlz {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] {n : ℕ} (p : LO.FirstOrder.Semiformula L M n) (e : Fin n → M) : Prop

Equations

• p.Rlz e = (LO.FirstOrder.Semiformula.Evalm M e id) p

@[simp]

theorem LO.FirstOrder.models₀_not_iff {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [LO.FirstOrder.Structure L M] (σ : LO.FirstOrder.Sentence L) : M ⊧ₘ₀ ∼σ ↔ ¬M ⊧ₘ₀ σ

@[simp]

theorem LO.FirstOrder.models₀_or_iff {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [LO.FirstOrder.Structure L M] (σ : LO.FirstOrder.Sentence L) (π : LO.FirstOrder.Sentence L) : M ⊧ₘ₀ σ ⋎ π ↔ M ⊧ₘ₀ σ ∨ M ⊧ₘ₀ π

@[simp]

theorem LO.FirstOrder.models₀_imply_iff {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [LO.FirstOrder.Structure L M] (σ : LO.FirstOrder.Sentence L) (π : LO.FirstOrder.Sentence L) : M ⊧ₘ₀ σ ➝ π ↔ M ⊧ₘ₀ σ → M ⊧ₘ₀ π

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.exItr {L : LO.FirstOrder.Language} [L.LT] {μ : Type v} {s : ℕ} {n : ℕ} {k : ℕ} {p : LO.FirstOrder.Semiformula L μ (n + k)} : LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) (∃^[k] p) ↔ LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) p

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.univItr {L : LO.FirstOrder.Language} [L.LT] {μ : Type v} {s : ℕ} {n : ℕ} {k : ℕ} {p : LO.FirstOrder.Semiformula L μ (n + k)} : LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) (∀^[k] p) ↔ LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) p

instance LO.FirstOrder.Arith.instModelsTheoryCobhamR0_arithmetization (M : Type u_1) [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : M ⊧ₘ* 𝐑₀

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.Arith.nat_extention_sigmaOne (M : Type u_1) [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {σ : LO.FirstOrder.Sentence ℒₒᵣ} (hσ : LO.FirstOrder.Arith.Hierarchy 𝚺 1 σ) : ℕ ⊧ₘ₀ σ → M ⊧ₘ₀ σ

theorem LO.FirstOrder.Arith.nat_extention_piOne (M : Type u_1) [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {σ : LO.FirstOrder.Sentence ℒₒᵣ} (hσ : LO.FirstOrder.Arith.Hierarchy 𝚷 1 σ) : M ⊧ₘ₀ σ → ℕ ⊧ₘ₀ σ

theorem LO.Arith.bold_sigma_one_completeness' {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐑₀] {n : ℕ} {σ : LO.FirstOrder.Semisentence ℒₒᵣ n} (hσ : LO.FirstOrder.Arith.Hierarchy 𝚺 1 σ) {e : Fin n → ℕ} : ℕ ⊧/e σ → (M ⊧/fun (x : Fin n) => LO.ORingStruc.numeral (e x)) σ

@[simp]

theorem Mathlib.Vector.nil_get {α : Type u_1} (v : Mathlib.Vector α 0) : v.get = ![]