Hereditary Finite Set Theory in $\mathsf{I}{\mathrm{\Sigma }}_1$

@[simp]

theorem LO.Arith.susbset_insert {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (a : V) : a ⊆ insert x a

@[simp]

theorem LO.Arith.bitRemove_susbset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (a : V) : LO.Arith.bitRemove x a ⊆ a

theorem LO.Arith.lt_of_mem_dom {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {m : V} (h : ⟪x, y⟫ ∈ m) : x < m

theorem LO.Arith.lt_of_mem_rng {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {m : V} (h : ⟪x, y⟫ ∈ m) : y < m

theorem LO.Arith.insert_subset_insert_of_subset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (x : V) (h : a ⊆ b) : insert x a ⊆ insert x b

@[simp]

theorem LO.Arith.under_subset_under_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} : LO.Arith.under i ⊆ LO.Arith.under j ↔ i ≤ j

theorem LO.Arith.sUnion_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : ∃! u : V, ∀ (x : V), x ∈ u ↔ ∃ t ∈ s, x ∈ t

def LO.Arith.sUnion {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : V

Equations

• ⋃ʰᶠ s = Classical.choose! ⋯

def LO.Arith.«term⋃ʰᶠ_» : Lean.ParserDescr

Equations

• LO.Arith.«term⋃ʰᶠ_» = Lean.ParserDescr.node `LO.Arith.term⋃ʰᶠ_ 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃ʰᶠ ") (Lean.ParserDescr.cat `term 80))

@[simp]

theorem LO.Arith.mem_sUnion_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} : a ∈ ⋃ʰᶠ b ↔ ∃ c ∈ b, a ∈ c

@[simp]

theorem LO.Arith.sUnion_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ⋃ʰᶠ ∅ = ∅

theorem LO.Arith.sUnion_lt_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (ha : 0 < a) : ⋃ʰᶠ a < a

@[simp]

theorem LO.Arith.sUnion_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : ⋃ʰᶠ a ≤ a

theorem LO.Arith.sUnion_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {u : V} {s : V} : u = ⋃ʰᶠ s ↔ ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t

def LO.FirstOrder.Arith.sUnionDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.sUnion_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ fun (x : V) => ⋃ʰᶠ x via LO.FirstOrder.Arith.sUnionDef

@[simp]

theorem LO.Arith.sUnion_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.sUnionDef) ↔ v 0 = ⋃ʰᶠ v 1

instance LO.Arith.sUnion_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ fun (x : V) => ⋃ʰᶠ x

Equations

• ⋯ = ⋯

instance LO.Arith.sUnion_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₁ fun (x : V) => ⋃ʰᶠ x

Equations

• ⋯ = ⋯

def LO.Arith.union {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) : V

Equations

• LO.Arith.union a b = ⋃ʰᶠ {a, b}

def LO.Arith.instUnion_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : Union V

Equations

• LO.Arith.instUnion_arithmetization = { union := LO.Arith.union }

@[simp]

theorem LO.Arith.mem_cup_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} {c : V} : a ∈ b ∪ c ↔ a ∈ b ∨ a ∈ c

def LO.FirstOrder.Arith.unionDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.Arith.union_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ fun (x x_1 : V) => x ∪ x_1 via LO.FirstOrder.Arith.unionDef

@[simp]

theorem LO.Arith.union_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.unionDef) ↔ v 0 = v 1 ∪ v 2

instance LO.Arith.union_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ fun (x x_1 : V) => x ∪ x_1

Equations

• ⋯ = ⋯

instance LO.Arith.union_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₂ fun (x x_1 : V) => x ∪ x_1

Equations

• ⋯ = ⋯

theorem LO.Arith.insert_eq_union_singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (s : V) : insert a s = {a} ∪ s

@[simp]

theorem LO.Arith.union_polybound {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) : a ∪ b ≤ 2 * (a + b)

instance LO.Arith.instBounded₂Union {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.FirstOrder.Arith.Bounded₂ fun (x x_1 : V) => x ∪ x_1

Equations

• ⋯ = ⋯

theorem LO.Arith.union_comm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) : a ∪ b = b ∪ a

@[simp]

theorem LO.Arith.union_succ_union_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) : a ⊆ a ∪ b

@[simp]

theorem LO.Arith.union_succ_union_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) : b ⊆ a ∪ b

@[simp]

theorem LO.Arith.union_succ_union_union_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) (c : V) : a ⊆ a ∪ b ∪ c

@[simp]

theorem LO.Arith.union_succ_union_union_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) (c : V) : b ⊆ a ∪ b ∪ c

@[simp]

theorem LO.Arith.union_empty_eq_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : a ∪ ∅ = a

@[simp]

theorem LO.Arith.union_empty_eq_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : ∅ ∪ a = a

theorem LO.Arith.sInter_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : ∃! u : V, ∀ (x : V), x ∈ u ↔ s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t

def LO.Arith.sInter {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : V

Equations

• ⋂ʰᶠ s = Classical.choose! ⋯

def LO.Arith.«term⋂ʰᶠ_» : Lean.ParserDescr

Equations

• LO.Arith.«term⋂ʰᶠ_» = Lean.ParserDescr.node `LO.Arith.term⋂ʰᶠ_ 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂ʰᶠ ") (Lean.ParserDescr.cat `term 80))

theorem LO.Arith.mem_sInter_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {s : V} : x ∈ ⋂ʰᶠ s ↔ s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t

@[simp]

theorem LO.Arith.mem_sInter_iff_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ⋂ʰᶠ ∅ = ∅

theorem LO.Arith.mem_sInter_iff_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {s : V} (h : s ≠ ∅) : x ∈ ⋂ʰᶠ s ↔ ∀ t ∈ s, x ∈ t

def LO.Arith.inter {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) : V

Equations

• LO.Arith.inter a b = ⋂ʰᶠ {a, b}

def LO.Arith.instInter_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : Inter V

Equations

• LO.Arith.instInter_arithmetization = { inter := LO.Arith.inter }

@[simp]

theorem LO.Arith.mem_inter_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} {c : V} : a ∈ b ∩ c ↔ a ∈ b ∧ a ∈ c

theorem LO.Arith.inter_comm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) : a ∩ b = b ∩ a

theorem LO.Arith.inter_eq_self_of_subset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (h : a ⊆ b) : a ∩ b = a

theorem LO.Arith.product_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) : ∃! u : V, ∀ (x : V), x ∈ u ↔ ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫

def LO.Arith.product {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) : V

Equations

• a ×ʰᶠ b = Classical.choose! ⋯

def LO.Arith.«term_×ʰᶠ_» : Lean.TrailingParserDescr

Equations

• LO.Arith.«term_×ʰᶠ_» = Lean.ParserDescr.trailingNode `LO.Arith.term_×ʰᶠ_ 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ʰᶠ ") (Lean.ParserDescr.cat `term 61))

theorem LO.Arith.mem_product_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {a : V} {b : V} : x ∈ a ×ʰᶠ b ↔ ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫

theorem LO.Arith.mem_product_iff' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {a : V} {b : V} : x ∈ a ×ʰᶠ b ↔ π₁ x ∈ a ∧ π₂ x ∈ b

@[simp]

theorem LO.Arith.pair_mem_product_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {a : V} {b : V} : ⟪x, y⟫ ∈ a ×ʰᶠ b ↔ x ∈ a ∧ y ∈ b

theorem LO.Arith.pair_mem_product {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {a : V} {b : V} (hx : x ∈ a) (hy : y ∈ b) : ⟪x, y⟫ ∈ a ×ʰᶠ b

def LO.FirstOrder.Arith.productDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.Arith.product_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ fun (x x_1 : V) => x ×ʰᶠ x_1 via LO.FirstOrder.Arith.productDef

@[simp]

theorem LO.Arith.product_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.productDef) ↔ v 0 = v 1 ×ʰᶠ v 2

instance LO.Arith.product_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ fun (x x_1 : V) => x ×ʰᶠ x_1

Equations

• ⋯ = ⋯

instance LO.Arith.product_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₂ fun (x x_1 : V) => x ×ʰᶠ x_1

Equations

• ⋯ = ⋯

theorem LO.Arith.domain_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : ∃! d : V, ∀ (x : V), x ∈ d ↔ ∃ (y : V), ⟪x, y⟫ ∈ s

def LO.Arith.domain {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : V

Equations

• LO.Arith.domain s = Classical.choose! ⋯

Instances For

• LO.Arith.domain_definable
• LO.Arith.domain_definable'
• LO.Arith.instBounded₁Domain

theorem LO.Arith.mem_domain_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {s : V} : x ∈ LO.Arith.domain s ↔ ∃ (y : V), ⟪x, y⟫ ∈ s

def LO.FirstOrder.Arith.domainDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.domain_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.domain via LO.FirstOrder.Arith.domainDef

@[simp]

theorem LO.Arith.domain_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.domainDef) ↔ v 0 = LO.Arith.domain (v 1)

instance LO.Arith.domain_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.domain

Equations

• ⋯ = ⋯

instance LO.Arith.domain_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₁ LO.Arith.domain

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.domain_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.domain ∅ = ∅

@[simp]

theorem LO.Arith.domain_union {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) : LO.Arith.domain (a ∪ b) = LO.Arith.domain a ∪ LO.Arith.domain b

@[simp]

theorem LO.Arith.domain_singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) : LO.Arith.domain {⟪x, y⟫} = {x}

@[simp]

theorem LO.Arith.domain_insert {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) (s : V) : LO.Arith.domain (insert ⟪x, y⟫ s) = insert x (LO.Arith.domain s)

@[simp]

theorem LO.Arith.domain_bound {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : LO.Arith.domain s ≤ 2 * s

instance LO.Arith.instBounded₁Domain {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.FirstOrder.Arith.Bounded₁ LO.Arith.domain

Equations

• ⋯ = ⋯

theorem LO.Arith.mem_domain_of_pair_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {s : V} (h : ⟪x, y⟫ ∈ s) : x ∈ LO.Arith.domain s

theorem LO.Arith.domain_subset_domain_of_subset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {t : V} (h : s ⊆ t) : LO.Arith.domain s ⊆ LO.Arith.domain t

@[simp]

theorem LO.Arith.domain_eq_empty_iff_eq_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} : LO.Arith.domain s = ∅ ↔ s = ∅

Range

theorem LO.Arith.range_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : ∃! r : V, ∀ (y : V), y ∈ r ↔ ∃ (x : V), ⟪x, y⟫ ∈ s

def LO.Arith.range {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : V

Equations

• LO.Arith.range s = Classical.choose! ⋯

Instances For

• LO.Arith.range_definable
• LO.Arith.range_definable'

theorem LO.Arith.mem_range_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {y : V} {s : V} : y ∈ LO.Arith.range s ↔ ∃ (x : V), ⟪x, y⟫ ∈ s

def LO.FirstOrder.Arith.rangeDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.range_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.range via LO.FirstOrder.Arith.rangeDef

@[simp]

theorem LO.Arith.range_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.rangeDef) ↔ v 0 = LO.Arith.range (v 1)

instance LO.Arith.range_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.range

Equations

• ⋯ = ⋯

instance LO.Arith.range_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₁ LO.Arith.range

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.range_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.range ∅ = ∅

Disjoint

def LO.Arith.Disjoint {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (t : V) : Prop

Equations

• LO.Arith.Disjoint s t = (s ∩ t = ∅)

theorem LO.Arith.Disjoint.iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {t : V} : LO.Arith.Disjoint s t ↔ ∀ (x : V), x ∉ s ∨ x ∉ t

theorem LO.Arith.Disjoint.not_of_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {t : V} {x : V} (hs : x ∈ s) (ht : x ∈ t) : ¬LO.Arith.Disjoint s t

theorem LO.Arith.Disjoint.symm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {t : V} (h : LO.Arith.Disjoint s t) : LO.Arith.Disjoint t s

@[simp]

theorem LO.Arith.Disjoint.singleton_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {a : V} : LO.Arith.Disjoint {a} s ↔ a ∉ s

Mapping

def LO.Arith.IsMapping {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (m : V) : Prop

Equations

• LO.Arith.IsMapping m = ∀ x ∈ LO.Arith.domain m, ∃! y : V, ⟪x, y⟫ ∈ m

Instances For

• LO.Arith.isMapping_definable
• LO.Arith.isMapping_definable'

def LO.FirstOrder.Arith.isMappingDef : 𝚺₀.Semisentence 1

Equations

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

theorem LO.Arith.isMapping_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Predicate LO.Arith.IsMapping via LO.FirstOrder.Arith.isMappingDef

@[simp]

theorem LO.Arith.isMapping_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 1 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.isMappingDef) ↔ LO.Arith.IsMapping (v 0)

instance LO.Arith.isMapping_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Predicate LO.Arith.IsMapping

Equations

• ⋯ = ⋯

instance LO.Arith.isMapping_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Predicate LO.Arith.IsMapping

Equations

• ⋯ = ⋯

theorem LO.Arith.IsMapping.get_exists_uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} (h : LO.Arith.IsMapping m) {x : V} (hx : x ∈ LO.Arith.domain m) : ∃! y : V, ⟪x, y⟫ ∈ m

def LO.Arith.IsMapping.get {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} (h : LO.Arith.IsMapping m) {x : V} (hx : x ∈ LO.Arith.domain m) : V

Equations

• h.get hx = Classical.choose! ⋯

@[simp]

theorem LO.Arith.IsMapping.get_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} (h : LO.Arith.IsMapping m) {x : V} (hx : x ∈ LO.Arith.domain m) : ⟪x, h.get hx⟫ ∈ m

theorem LO.Arith.IsMapping.get_uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {y : V} {m : V} (h : LO.Arith.IsMapping m) {x : V} (hx : x ∈ LO.Arith.domain m) (hy : ⟪x, y⟫ ∈ m) : y = h.get hx

@[simp]

theorem LO.Arith.IsMapping.empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.IsMapping ∅

theorem LO.Arith.IsMapping.union_of_disjoint_domain {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m₁ : V} {m₂ : V} (h₁ : LO.Arith.IsMapping m₁) (h₂ : LO.Arith.IsMapping m₂) (disjoint : LO.Arith.Disjoint (LO.Arith.domain m₁) (LO.Arith.domain m₂)) : LO.Arith.IsMapping (m₁ ∪ m₂)

@[simp]

theorem LO.Arith.IsMapping.singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) : LO.Arith.IsMapping {⟪x, y⟫}

theorem LO.Arith.IsMapping.insert {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {m : V} (h : LO.Arith.IsMapping m) (disjoint : x ∉ LO.Arith.domain m) : LO.Arith.IsMapping (insert ⟪x, y⟫ m)

theorem LO.Arith.IsMapping.of_subset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} {m' : V} (h : LO.Arith.IsMapping m) (ss : m' ⊆ m) : LO.Arith.IsMapping m'

theorem LO.Arith.IsMapping.uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} {x : V} {y₁ : V} {y₂ : V} (h : LO.Arith.IsMapping m) : ⟪x, y₁⟫ ∈ m → ⟪x, y₂⟫ ∈ m → y₁ = y₂

Restriction of mapping

theorem LO.Arith.restr_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (f : V) (s : V) : ∃! g : V, ∀ (x : V), x ∈ g ↔ x ∈ f ∧ π₁ x ∈ s

def LO.Arith.restr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (f : V) (s : V) : V

Equations

• LO.Arith.restr f s = Classical.choose! ⋯

def LO.Arith.«term_↾_» : Lean.TrailingParserDescr

Equations

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

theorem LO.Arith.mem_restr_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {f : V} {s : V} : x ∈ LO.Arith.restr f s ↔ x ∈ f ∧ π₁ x ∈ s

@[simp]

theorem LO.Arith.pair_mem_restr_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {f : V} {s : V} : ⟪x, y⟫ ∈ LO.Arith.restr f s ↔ ⟪x, y⟫ ∈ f ∧ x ∈ s

@[simp]

theorem LO.Arith.restr_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (f : V) : LO.Arith.restr f ∅ = ∅

@[simp]

theorem LO.Arith.restr_subset_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (f : V) (s : V) : LO.Arith.restr f s ⊆ f

@[simp]

theorem LO.Arith.restr_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (f : V) (s : V) : LO.Arith.restr f s ≤ f

theorem LO.Arith.IsMapping.restr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} (h : LO.Arith.IsMapping m) (s : V) : LO.Arith.IsMapping (LO.Arith.restr m s)

theorem LO.Arith.domain_restr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (f : V) (s : V) : LO.Arith.domain (LO.Arith.restr f s) = LO.Arith.domain f ∩ s

theorem LO.Arith.domain_restr_of_subset_domain {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {f : V} {s : V} (h : s ⊆ LO.Arith.domain f) : LO.Arith.domain (LO.Arith.restr f s) = s

theorem LO.Arith.insert_induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hempty : P ∅) (hinsert : ∀ (a s : V), a ∉ s → P s → P (insert a s)) (s : V) : P s

theorem LO.Arith.insert_induction_sigmaOne {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : V → Prop} (hP : 𝚺₁-Predicate P) (hempty : P ∅) (hinsert : ∀ (a s : V), a ∉ s → P s → P (insert a s)) (s : V) : P s

theorem LO.Arith.insert_induction_piOne {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : V → Prop} (hP : 𝚷₁-Predicate P) (hempty : P ∅) (hinsert : ∀ (a s : V), a ∉ s → P s → P (insert a s)) (s : V) : P s

theorem LO.Arith.sigmaOne_skolem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {R : V → V → Prop} (hP : 𝚺₁-Relation R) {s : V} (H : ∀ x ∈ s, ∃ (y : V), R x y) : ∃ (f : V), LO.Arith.IsMapping f ∧ LO.Arith.domain f = s ∧ ∀ (x y : V), ⟪x, y⟫ ∈ f → R x y

theorem LO.Arith.sigma₁_replacement {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {f : V → V} (hf : 𝚺₁-Function₁ f) (s : V) : ∃! t : V, ∀ (y : V), y ∈ t ↔ ∃ x ∈ s, y = f x

theorem LO.Arith.sigma₁_replacement₂ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {f : V → V → V} (hf : 𝚺₁-Function₂ f) (s₁ : V) (s₂ : V) : ∃! t : V, ∀ (y : V), y ∈ t ↔ ∃ x₁ ∈ s₁, ∃ x₂ ∈ s₂, y = f x₁ x₂

def LO.Arith.fstIdx {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) : V

Equations

• LO.Arith.fstIdx p = π₁(p - 1)

Instances For

• LO.Arith.fstIdx_definable
• LO.Arith.fstIdx_definable'

@[simp]

theorem LO.Arith.fstIdx_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) : LO.Arith.fstIdx p ≤ p

def LO.FirstOrder.Arith.fstIdxDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.fstIdx_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.fstIdx via LO.FirstOrder.Arith.fstIdxDef

@[simp]

theorem LO.Arith.eval_fstIdxDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.fstIdxDef) ↔ v 0 = LO.Arith.fstIdx (v 1)

instance LO.Arith.fstIdx_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.fstIdx

Equations

• ⋯ = ⋯

instance LO.Arith.fstIdx_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.FirstOrder.Arith.HierarchySymbol) : Γ-Function₁ LO.Arith.fstIdx

Equations

• ⋯ = ⋯

def LO.Arith.sndIdx {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) : V

Equations

• LO.Arith.sndIdx p = π₂(p - 1)

Instances For

• LO.Arith.sndIdx_definable
• LO.Arith.sndIdx_definable'

@[simp]

theorem LO.Arith.sndIdx_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) : LO.Arith.sndIdx p ≤ p

def LO.FirstOrder.Arith.sndIdxDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.sndIdx_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.sndIdx via LO.FirstOrder.Arith.sndIdxDef

@[simp]

theorem LO.Arith.eval_sndIdxDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.sndIdxDef) ↔ v 0 = LO.Arith.sndIdx (v 1)

instance LO.Arith.sndIdx_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.sndIdx

Equations

• ⋯ = ⋯

instance LO.Arith.sndIdx_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.FirstOrder.Arith.HierarchySymbol) : Γ-Function₁ LO.Arith.sndIdx

Equations

• ⋯ = ⋯