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

@[simp]

theorem LO.FirstOrder.Arithmetic.susbset_insert {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x a : V) : a ⊆ insert x a

@[simp]

theorem LO.FirstOrder.Arithmetic.bitRemove_susbset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x a : V) : bitRemove x a ⊆ a

theorem LO.FirstOrder.Arithmetic.lt_of_mem_dom {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x y m : V} (h : ⟪x, y⟫ ∈ m) : x < m

theorem LO.FirstOrder.Arithmetic.lt_of_mem_rng {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x y m : V} (h : ⟪x, y⟫ ∈ m) : y < m

theorem LO.FirstOrder.Arithmetic.insert_subset_insert_of_subset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} (x : V) (h : a ⊆ b) : insert x a ⊆ insert x b

@[simp]

theorem LO.FirstOrder.Arithmetic.under_subset_under_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i j : V} : under i ⊆ under j ↔ i ≤ j

theorem LO.FirstOrder.Arithmetic.sUnion_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : ∃! u : V, ∀ (x : V), x ∈ u ↔ ∃ t ∈ s, x ∈ t

noncomputable def LO.FirstOrder.Arithmetic.sUnion {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : V

Equations

• ⋃ʰᶠ s = Classical.choose! ⋯

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

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.mem_sUnion_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} : a ∈ ⋃ʰᶠ b ↔ ∃ c ∈ b, a ∈ c

@[simp]

theorem LO.FirstOrder.Arithmetic.sUnion_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ⋃ʰᶠ ∅ = ∅

theorem LO.FirstOrder.Arithmetic.sUnion_lt_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a : V} (ha : 0 < a) : ⋃ʰᶠ a < a

@[simp]

theorem LO.FirstOrder.Arithmetic.sUnion_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : ⋃ʰᶠ a ≤ a

theorem LO.FirstOrder.Arithmetic.sUnion_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {u s : V} : u = ⋃ʰᶠ s ↔ ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t

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

Equations

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

instance LO.FirstOrder.Arithmetic.sUnion_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ sUnion via sUnionDef

instance LO.FirstOrder.Arithmetic.sUnion_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ sUnion

instance LO.FirstOrder.Arithmetic.sUnion_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₁ sUnion

noncomputable def LO.FirstOrder.Arithmetic.union {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : V

Equations

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

@[implicit_reducible]

noncomputable def LO.FirstOrder.Arithmetic.instUnion_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Union V

Equations

• LO.FirstOrder.Arithmetic.instUnion_foundation = { union := LO.FirstOrder.Arithmetic.union }

@[simp]

theorem LO.FirstOrder.Arithmetic.mem_cup_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b c : V} : a ∈ b ∪ c ↔ a ∈ b ∨ a ∈ c

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

Equations

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

instance LO.FirstOrder.Arithmetic.union_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₂ fun (x1 x2 : V) => x1 ∪ x2 via unionDef

instance LO.FirstOrder.Arithmetic.union_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₂ fun (x1 x2 : V) => x1 ∪ x2

instance LO.FirstOrder.Arithmetic.union_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₂ fun (x1 x2 : V) => x1 ∪ x2

theorem LO.FirstOrder.Arithmetic.insert_eq_union_singleton {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a s : V) : insert a s = {a} ∪ s

@[simp]

theorem LO.FirstOrder.Arithmetic.union_polybound {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : a ∪ b ≤ 2 * (a + b)

instance LO.FirstOrder.Arithmetic.instBounded₂Union {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Bounded₂ fun (x1 x2 : V) => x1 ∪ x2

theorem LO.FirstOrder.Arithmetic.union_comm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : a ∪ b = b ∪ a

@[simp]

theorem LO.FirstOrder.Arithmetic.union_succ_union_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : a ⊆ a ∪ b

@[simp]

theorem LO.FirstOrder.Arithmetic.union_succ_union_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : b ⊆ a ∪ b

@[simp]

theorem LO.FirstOrder.Arithmetic.union_succ_union_union_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b c : V) : a ⊆ a ∪ b ∪ c

@[simp]

theorem LO.FirstOrder.Arithmetic.union_succ_union_union_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b c : V) : b ⊆ a ∪ b ∪ c

@[simp]

theorem LO.FirstOrder.Arithmetic.union_empty_eq_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : a ∪ ∅ = a

@[simp]

theorem LO.FirstOrder.Arithmetic.union_empty_eq_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : ∅ ∪ a = a

theorem LO.FirstOrder.Arithmetic.sInter_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : ∃! u : V, ∀ (x : V), x ∈ u ↔ s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t

noncomputable def LO.FirstOrder.Arithmetic.sInter {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : V

Equations

• ⋂ʰᶠ s = Classical.choose! ⋯

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

Equations

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

theorem LO.FirstOrder.Arithmetic.mem_sInter_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x s : V} : x ∈ ⋂ʰᶠ s ↔ s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t

@[simp]

theorem LO.FirstOrder.Arithmetic.mem_sInter_iff_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ⋂ʰᶠ ∅ = ∅

theorem LO.FirstOrder.Arithmetic.mem_sInter_iff_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x s : V} (h : s ≠ ∅) : x ∈ ⋂ʰᶠ s ↔ ∀ t ∈ s, x ∈ t

noncomputable def LO.FirstOrder.Arithmetic.inter {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : V

Equations

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

@[implicit_reducible]

noncomputable def LO.FirstOrder.Arithmetic.instInter_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Inter V

Equations

• LO.FirstOrder.Arithmetic.instInter_foundation = { inter := LO.FirstOrder.Arithmetic.inter }

@[simp]

theorem LO.FirstOrder.Arithmetic.mem_inter_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b c : V} : a ∈ b ∩ c ↔ a ∈ b ∧ a ∈ c

theorem LO.FirstOrder.Arithmetic.inter_comm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : a ∩ b = b ∩ a

theorem LO.FirstOrder.Arithmetic.inter_eq_self_of_subset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} (h : a ⊆ b) : a ∩ b = a

theorem LO.FirstOrder.Arithmetic.product_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : ∃! u : V, ∀ (x : V), x ∈ u ↔ ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫

noncomputable def LO.FirstOrder.Arithmetic.product {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : V

Equations

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

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

Equations

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

theorem LO.FirstOrder.Arithmetic.mem_product_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x a b : V} : x ∈ a ×ʰᶠ b ↔ ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫

theorem LO.FirstOrder.Arithmetic.mem_product_iff' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x a b : V} : x ∈ a ×ʰᶠ b ↔ π₁ x ∈ a ∧ π₂ x ∈ b

@[simp]

theorem LO.FirstOrder.Arithmetic.pair_mem_product_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x y a b : V} : ⟪x, y⟫ ∈ a ×ʰᶠ b ↔ x ∈ a ∧ y ∈ b

theorem LO.FirstOrder.Arithmetic.pair_mem_product {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x y a b : V} (hx : x ∈ a) (hy : y ∈ b) : ⟪x, y⟫ ∈ a ×ʰᶠ b

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

Equations

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

instance LO.FirstOrder.Arithmetic.product_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₂ fun (x1 x2 : V) => x1 ×ʰᶠ x2 via productDef

instance LO.FirstOrder.Arithmetic.product_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₂ fun (x1 x2 : V) => x1 ×ʰᶠ x2

instance LO.FirstOrder.Arithmetic.product_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₂ fun (x1 x2 : V) => x1 ×ʰᶠ x2

theorem LO.FirstOrder.Arithmetic.domain_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : ∃! d : V, ∀ (x : V), x ∈ d ↔ ∃ (y : V), ⟪x, y⟫ ∈ s

noncomputable def LO.FirstOrder.Arithmetic.domain {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : V

Equations

• LO.FirstOrder.Arithmetic.domain s = Classical.choose! ⋯

theorem LO.FirstOrder.Arithmetic.mem_domain_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x s : V} : x ∈ domain s ↔ ∃ (y : V), ⟪x, y⟫ ∈ s

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

Equations

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

instance LO.FirstOrder.Arithmetic.domain_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ domain via domainDef

instance LO.FirstOrder.Arithmetic.domain_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ domain

instance LO.FirstOrder.Arithmetic.domain_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₁ domain

@[simp]

theorem LO.FirstOrder.Arithmetic.domain_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : domain ∅ = ∅

@[simp]

theorem LO.FirstOrder.Arithmetic.domain_union {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : domain (a ∪ b) = domain a ∪ domain b

@[simp]

theorem LO.FirstOrder.Arithmetic.domain_singleton {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x y : V) : domain {⟪x, y⟫} = {x}

@[simp]

theorem LO.FirstOrder.Arithmetic.domain_insert {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x y s : V) : domain (insert ⟪x, y⟫ s) = insert x (domain s)

@[simp]

theorem LO.FirstOrder.Arithmetic.domain_bound {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : domain s ≤ 2 * s

instance LO.FirstOrder.Arithmetic.instBounded₁Domain {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Bounded₁ domain

theorem LO.FirstOrder.Arithmetic.mem_domain_of_pair_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x y s : V} (h : ⟪x, y⟫ ∈ s) : x ∈ domain s

theorem LO.FirstOrder.Arithmetic.domain_subset_domain_of_subset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {s t : V} (h : s ⊆ t) : domain s ⊆ domain t

@[simp]

theorem LO.FirstOrder.Arithmetic.domain_eq_empty_iff_eq_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {s : V} : domain s = ∅ ↔ s = ∅

Range

theorem LO.FirstOrder.Arithmetic.range_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : ∃! r : V, ∀ (y : V), y ∈ r ↔ ∃ (x : V), ⟪x, y⟫ ∈ s

noncomputable def LO.FirstOrder.Arithmetic.range {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : V

Equations

• LO.FirstOrder.Arithmetic.range s = Classical.choose! ⋯

theorem LO.FirstOrder.Arithmetic.mem_range_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {y s : V} : y ∈ range s ↔ ∃ (x : V), ⟪x, y⟫ ∈ s

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

Equations

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

instance LO.FirstOrder.Arithmetic.range_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ range via rangeDef

instance LO.FirstOrder.Arithmetic.range_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ range

instance LO.FirstOrder.Arithmetic.range_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₁ range

@[simp]

theorem LO.FirstOrder.Arithmetic.range_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : range ∅ = ∅

Disjoint

def LO.FirstOrder.Arithmetic.Disjoint {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s t : V) : Prop

Equations

• LO.FirstOrder.Arithmetic.Disjoint s t = (s ∩ t = ∅)

theorem LO.FirstOrder.Arithmetic.Disjoint.iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {s t : V} : Disjoint s t ↔ ∀ (x : V), x ∉ s ∨ x ∉ t

theorem LO.FirstOrder.Arithmetic.Disjoint.not_of_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {s t x : V} (hs : x ∈ s) (ht : x ∈ t) : ¬Disjoint s t

theorem LO.FirstOrder.Arithmetic.Disjoint.symm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {s t : V} (h : Disjoint s t) : Disjoint t s

@[simp]

theorem LO.FirstOrder.Arithmetic.Disjoint.singleton_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {s a : V} : Disjoint {a} s ↔ a ∉ s

Mapping

def LO.FirstOrder.Arithmetic.IsMapping {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (m : V) : Prop

Equations

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

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

Equations

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

instance LO.FirstOrder.Arithmetic.isMapping_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Predicate IsMapping via isMappingDef

instance LO.FirstOrder.Arithmetic.isMapping_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Predicate IsMapping

instance LO.FirstOrder.Arithmetic.isMapping_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Predicate IsMapping

theorem LO.FirstOrder.Arithmetic.IsMapping.get_exists_uniq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m : V} (h : IsMapping m) {x : V} (hx : x ∈ domain m) : ∃! y : V, ⟪x, y⟫ ∈ m

noncomputable def LO.FirstOrder.Arithmetic.IsMapping.get {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m : V} (h : IsMapping m) {x : V} (hx : x ∈ domain m) : V

Equations

• h.get hx = Classical.choose! ⋯

@[simp]

theorem LO.FirstOrder.Arithmetic.IsMapping.get_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m : V} (h : IsMapping m) {x : V} (hx : x ∈ domain m) : ⟪x, h.get hx⟫ ∈ m

theorem LO.FirstOrder.Arithmetic.IsMapping.get_uniq {V : Type u_1} [ORingStructure 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.FirstOrder.Arithmetic.IsMapping.empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : IsMapping ∅

theorem LO.FirstOrder.Arithmetic.IsMapping.union_of_disjoint_domain {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m₁ m₂ : V} (h₁ : IsMapping m₁) (h₂ : IsMapping m₂) (disjoint : Disjoint (domain m₁) (domain m₂)) : IsMapping (m₁ ∪ m₂)

@[simp]

theorem LO.FirstOrder.Arithmetic.IsMapping.singleton {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x y : V) : IsMapping {⟪x, y⟫}

theorem LO.FirstOrder.Arithmetic.IsMapping.insert {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x y m : V} (h : IsMapping m) (disjoint : x ∉ domain m) : IsMapping (Insert.insert ⟪x, y⟫ m)

theorem LO.FirstOrder.Arithmetic.IsMapping.of_subset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m m' : V} (h : IsMapping m) (ss : m' ⊆ m) : IsMapping m'

theorem LO.FirstOrder.Arithmetic.IsMapping.uniq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m x y₁ y₂ : V} (h : IsMapping m) : ⟪x, y₁⟫ ∈ m → ⟪x, y₂⟫ ∈ m → y₁ = y₂

Restriction of mapping

theorem LO.FirstOrder.Arithmetic.restr_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (f s : V) : ∃! g : V, ∀ (x : V), x ∈ g ↔ x ∈ f ∧ π₁ x ∈ s

noncomputable def LO.FirstOrder.Arithmetic.restr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (f s : V) : V

Equations

• LO.FirstOrder.Arithmetic.restr f s = Classical.choose! ⋯

def LO.FirstOrder.Arithmetic.«term_↾_» : Lean.TrailingParserDescr

Equations

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

theorem LO.FirstOrder.Arithmetic.mem_restr_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x f s : V} : x ∈ restr f s ↔ x ∈ f ∧ π₁ x ∈ s

@[simp]

theorem LO.FirstOrder.Arithmetic.pair_mem_restr_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x y f s : V} : ⟪x, y⟫ ∈ restr f s ↔ ⟪x, y⟫ ∈ f ∧ x ∈ s

@[simp]

theorem LO.FirstOrder.Arithmetic.restr_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (f : V) : restr f ∅ = ∅

@[simp]

theorem LO.FirstOrder.Arithmetic.restr_subset_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (f s : V) : restr f s ⊆ f

@[simp]

theorem LO.FirstOrder.Arithmetic.restr_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (f s : V) : restr f s ≤ f

theorem LO.FirstOrder.Arithmetic.IsMapping.restr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m : V} (h : IsMapping m) (s : V) : IsMapping (Arithmetic.restr m s)

theorem LO.FirstOrder.Arithmetic.domain_restr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (f s : V) : domain (restr f s) = domain f ∩ s

theorem LO.FirstOrder.Arithmetic.domain_restr_of_subset_domain {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {f s : V} (h : s ⊆ domain f) : domain (restr f s) = s

theorem LO.FirstOrder.Arithmetic.insert_induction {V : Type u_1} [ORingStructure 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.FirstOrder.Arithmetic.insert_induction_sigmaOne {V : Type u_1} [ORingStructure 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.FirstOrder.Arithmetic.insert_induction_piOne {V : Type u_1} [ORingStructure 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.FirstOrder.Arithmetic.sigmaOne_skolem {V : Type u_1} [ORingStructure 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.FirstOrder.Arithmetic.sigma₁_replacement {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {f : V → V} (hf : 𝚺₁-Function₁ f) (s : V) : ∃! t : V, ∀ (y : V), y ∈ t ↔ ∃ x ∈ s, y = f x

theorem LO.FirstOrder.Arithmetic.sigma₁_replacement₂ {V : Type u_1} [ORingStructure 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₂

Image of HFS

noncomputable def LO.FirstOrder.Arithmetic.hfsImage {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (f : V → V) [𝚺₁-Function₁ f] (s : V) : V

Equations

• LO.FirstOrder.Arithmetic.hfsImage f s = Classical.choose! ⋯

theorem LO.FirstOrder.Arithmetic.mem_hfsImage_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {f : V → V} [𝚺₁-Function₁ f] {s y : V} : y ∈ hfsImage f s ↔ ∃ x ∈ s, y = f x

theorem LO.FirstOrder.Arithmetic.app_mem_hfsImage {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {f : V → V} [𝚺₁-Function₁ f] {p s : V} (h : p ∈ s) : f p ∈ hfsImage f s

theorem LO.FirstOrder.Arithmetic.hfsImage_subset_of_subset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {f : V → V} [𝚺₁-Function₁ f] {s t : V} (h : s ⊆ t) : hfsImage f s ⊆ hfsImage f t

@[simp]

theorem LO.FirstOrder.Arithmetic.mem_hfsImage_union {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {f : V → V} [𝚺₁-Function₁ f] {s t : V} : hfsImage f (s ∪ t) = hfsImage f s ∪ hfsImage f t

@[simp]

theorem LO.FirstOrder.Arithmetic.mem_hfsImage_insert {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {f : V → V} [𝚺₁-Function₁ f] {x s : V} : hfsImage f (insert x s) = insert (f x) (hfsImage f s)

@[simp]

theorem LO.FirstOrder.Arithmetic.hfsImage_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {f : V → V} [𝚺₁-Function₁ f] : hfsImage f ∅ = ∅

noncomputable def LO.FirstOrder.Arithmetic.hfsImage.graph (δ : 𝚺₁.Semisentence 2) : 𝚺₁.Semisentence 2

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.hfsImage.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (f : V → V) [𝚺₁-Function₁ f] (δ : 𝚺₁.Semisentence 2) [𝚺₁-Function₁ f via δ] : 𝚺₁-Function₁ hfsImage f via graph δ

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.hfsImage.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (f : V → V) [𝚺₁-Function₁ f] (δ : 𝚺₁.Semisentence 2) [𝚺₁-Function₁ f via δ] : 𝚺₁-Function₁ hfsImage f

Equations

• ⋯ = ⋯

noncomputable def LO.FirstOrder.Arithmetic.fstIdx {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : V

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.fstIdx_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : fstIdx p ≤ p

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

Equations

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

instance LO.FirstOrder.Arithmetic.fstIdx_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ fstIdx via fstIdxDef

instance LO.FirstOrder.Arithmetic.fstIdx_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ fstIdx

instance LO.FirstOrder.Arithmetic.fstIdx_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (Γ : HierarchySymbol) : Γ-Function₁ fstIdx

noncomputable def LO.FirstOrder.Arithmetic.sndIdx {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : V

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.sndIdx_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : sndIdx p ≤ p

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

Equations

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

instance LO.FirstOrder.Arithmetic.sndIdx_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ sndIdx via sndIdxDef

instance LO.FirstOrder.Arithmetic.sndIdx_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ sndIdx

instance LO.FirstOrder.Arithmetic.sndIdx_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (Γ : HierarchySymbol) : Γ-Function₁ sndIdx