Hereditary Finite Set Theory in $\mathsf{I} \Sigma_1$

@[simp]

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

@[simp]

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

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

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

theorem LO.Arith.insert_subset_insert_of_subset {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i j : V} : under i ⊆ under j ↔ i ≤ j

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

def LO.Arith.sUnion {V : Type u_1} [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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a b : V} : a ∈ ⋃ʰᶠ b ↔ ∃ c ∈ b, a ∈ c

@[simp]

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

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

@[simp]

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

theorem LO.Arith.sUnion_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {u 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ fun (x : V) => ⋃ʰᶠ x via FirstOrder.Arith.sUnionDef

@[simp]

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

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

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

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

Equations

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

def LO.Arith.instUnion_arithmetization {V : Type u_1} [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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a b 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ fun (x1 x2 : V) => x1 ∪ x2 via FirstOrder.Arith.unionDef

@[simp]

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

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

def LO.Arith.sInter {V : Type u_1} [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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x s : V} : x ∈ ⋂ʰᶠ s ↔ s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t

@[simp]

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

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

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

Equations

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

def LO.Arith.instInter_arithmetization {V : Type u_1} [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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a b c : V} : a ∈ b ∩ c ↔ a ∈ b ∧ a ∈ c

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

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

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

def LO.Arith.product {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x a b : V} : x ∈ a ×ʰᶠ b ↔ ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫

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

@[simp]

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

theorem LO.Arith.pair_mem_product {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x y a 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ fun (x1 x2 : V) => x1 ×ʰᶠ x2 via FirstOrder.Arith.productDef

@[simp]

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

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

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

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

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

Equations

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

theorem LO.Arith.mem_domain_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x s : V} : x ∈ 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ domain via FirstOrder.Arith.domainDef

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

Range

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

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

Equations

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

theorem LO.Arith.mem_range_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {y s : V} : y ∈ 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ range via FirstOrder.Arith.rangeDef

@[simp]

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

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

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

@[simp]

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

Disjoint

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

Equations

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

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

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

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

@[simp]

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

Mapping

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

Equations

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

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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Predicate IsMapping via FirstOrder.Arith.isMappingDef

@[simp]

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

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

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

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

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

Equations

• h.get hx = Classical.choose! ⋯

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

Restriction of mapping

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

def LO.Arith.restr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (f 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x f s : V} : x ∈ restr f s ↔ x ∈ f ∧ π₁ x ∈ s

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

Equations

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

@[simp]

theorem LO.Arith.fstIdx_le_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ fstIdx via FirstOrder.Arith.fstIdxDef

@[simp]

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

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

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

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

Equations

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

@[simp]

theorem LO.Arith.sndIdx_le_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ sndIdx via FirstOrder.Arith.sndIdxDef

@[simp]

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

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

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