Hereditary Finite Set Theory in $\mathsf{I} \Sigma_1$ #
@[simp]
@[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)
:
@[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
Equations
- ⋃ʰᶠ s = Classical.choose! ⋯
Instances For
Equations
- LO.Arith.«term⋃ʰᶠ_» = Lean.ParserDescr.node `LO.Arith.term⋃ʰᶠ_ 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃ʰᶠ ") (Lean.ParserDescr.cat `term 80))
Instances For
@[simp]
theorem
LO.Arith.sUnion_lt_of_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{a : V}
(ha : 0 < a)
:
@[simp]
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.sUnion_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ fun (x : V) => ⋃ʰᶠ x via LO.FirstOrder.Arith.sUnionDef
@[simp]
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
- ⋯ = ⋯
Equations
- LO.Arith.union a b = ⋃ʰᶠ {a, b}
Instances For
Equations
- LO.Arith.instUnion_arithmetization = { union := LO.Arith.union }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
@[simp]
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
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.union_succ_union_left
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(a : V)
(b : V)
:
@[simp]
theorem
LO.Arith.union_succ_union_right
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(a : V)
(b : V)
:
@[simp]
theorem
LO.Arith.union_succ_union_union_left
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(a : V)
(b : V)
(c : V)
:
@[simp]
theorem
LO.Arith.union_succ_union_union_right
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(a : V)
(b : V)
(c : V)
:
@[simp]
@[simp]
Equations
- ⋂ʰᶠ s = Classical.choose! ⋯
Instances For
Equations
- LO.Arith.«term⋂ʰᶠ_» = Lean.ParserDescr.node `LO.Arith.term⋂ʰᶠ_ 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂ʰᶠ ") (Lean.ParserDescr.cat `term 80))
Instances For
@[simp]
Equations
- LO.Arith.inter a b = ⋂ʰᶠ {a, b}
Instances For
Equations
- LO.Arith.instInter_arithmetization = { inter := LO.Arith.inter }
Instances For
theorem
LO.Arith.inter_eq_self_of_subset
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{a : V}
{b : V}
(h : a ⊆ b)
:
theorem
LO.Arith.product_exists_unique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(a : V)
(b : V)
:
Equations
- a ×ʰᶠ b = Classical.choose! ⋯
Instances For
Equations
- LO.Arith.«term_×ʰᶠ_» = Lean.ParserDescr.trailingNode `LO.Arith.term_×ʰᶠ_ 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ʰᶠ ") (Lean.ParserDescr.cat `term 61))
Instances For
theorem
LO.Arith.mem_product_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{x : V}
{a : V}
{b : V}
:
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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- ⋯ = ⋯
Equations
Instances For
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.domain_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ LO.Arith.domain via LO.FirstOrder.Arith.domainDef
@[simp]
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]
@[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)
:
@[simp]
theorem
LO.Arith.domain_eq_empty_iff_eq_empty
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
:
Range #
Equations
Instances For
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.range_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ LO.Arith.range via LO.FirstOrder.Arith.rangeDef
@[simp]
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]
Disjoint #
Equations
- LO.Arith.Disjoint s t = (s ∩ t = ∅)
Instances For
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)
:
theorem
LO.Arith.Disjoint.symm
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
{t : V}
(h : LO.Arith.Disjoint s t)
:
@[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 #
Equations
- LO.Arith.IsMapping m = ∀ x ∈ LO.Arith.domain m, ∃! y : V, ⟪x, y⟫ ∈ m
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
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! ⋯
Instances For
@[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.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)
:
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)
:
Restriction of mapping #
Equations
- LO.Arith.restr f s = Classical.choose! ⋯
Instances For
Equations
- LO.Arith.«term_↾_» = Lean.ParserDescr.trailingNode `LO.Arith.term_↾_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↾ ") (Lean.ParserDescr.cat `term 81))
Instances For
theorem
LO.Arith.mem_restr_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{x : V}
{f : V}
{s : V}
:
@[simp]
theorem
LO.Arith.pair_mem_restr_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{x : V}
{y : V}
{f : V}
{s : V}
:
@[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)
:
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)
:
theorem
LO.Arith.sigma₁_replacement₂
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{f : V → V → V}
(hf : 𝚺₁-Function₂ f)
(s₁ : V)
(s₂ : V)
:
Equations
- LO.Arith.fstIdx p = π₁(p - 1)
Instances For
@[simp]
theorem
LO.Arith.fstIdx_le_self
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p : V)
:
LO.Arith.fstIdx p ≤ p
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.fstIdx_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ LO.Arith.fstIdx via LO.FirstOrder.Arith.fstIdxDef
@[simp]
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
- ⋯ = ⋯
Equations
- LO.Arith.sndIdx p = π₂(p - 1)
Instances For
@[simp]
theorem
LO.Arith.sndIdx_le_self
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p : V)
:
LO.Arith.sndIdx p ≤ p
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.sndIdx_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ LO.Arith.sndIdx via LO.FirstOrder.Arith.sndIdxDef
@[simp]
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
- ⋯ = ⋯