Sequence #
Equations
- LO.Arith.Seq s = (LO.Arith.IsMapping s ∧ ∃ (l : V), LO.Arith.domain s = LO.Arith.under l)
Instances For
def
LO.Arith.Seq.isMapping
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : LO.Arith.Seq s)
:
Equations
- ⋯ = ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.seq_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Predicate LO.Arith.Seq via LO.FirstOrder.Arith.seqDef
@[simp]
instance
LO.Arith.seq_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Predicate LO.Arith.Seq
Equations
- ⋯ = ⋯
instance
LO.Arith.seq_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Predicate LO.Arith.Seq
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.lh_exists_uniq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
:
∃! l : V, (LO.Arith.Seq s → LO.Arith.domain s = LO.Arith.under l) ∧ (¬LO.Arith.Seq s → l = 0)
Equations
Instances For
theorem
LO.Arith.lh_prop
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
:
(LO.Arith.Seq s → LO.Arith.domain s = LO.Arith.under (LO.Arith.lh s)) ∧ (¬LO.Arith.Seq s → LO.Arith.lh s = 0)
theorem
LO.Arith.lh_prop_of_not_seq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : ¬LO.Arith.Seq s)
:
LO.Arith.lh s = 0
theorem
LO.Arith.Seq.domain_eq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : LO.Arith.Seq s)
:
@[simp]
theorem
LO.Arith.lh_bound
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
:
LO.Arith.lh s ≤ 2 * s
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.lh_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ LO.Arith.lh via LO.FirstOrder.Arith.lhDef
@[simp]
instance
LO.Arith.lh_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ LO.Arith.lh
Equations
- ⋯ = ⋯
instance
LO.Arith.lh_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₁ LO.Arith.lh
Equations
- ⋯ = ⋯
instance
LO.Arith.instBounded₁Lh
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
LO.FirstOrder.Arith.Bounded₁ LO.Arith.lh
Equations
- ⋯ = ⋯
theorem
LO.Arith.Seq.exists
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : LO.Arith.Seq s)
{x : V}
(hx : x < LO.Arith.lh s)
:
∃ (y : V), ⟪x, y⟫ ∈ s
theorem
LO.Arith.Seq.nth_exists_uniq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : LO.Arith.Seq s)
{x : V}
(hx : x < LO.Arith.lh s)
:
∃! y : V, ⟪x, y⟫ ∈ s
def
LO.Arith.Seq.nth
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : LO.Arith.Seq s)
{x : V}
(hx : x < LO.Arith.lh s)
:
V
Equations
- h.nth hx = Classical.choose! ⋯
Instances For
@[simp]
theorem
LO.Arith.Seq.nth_mem
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : LO.Arith.Seq s)
{x : V}
(hx : x < LO.Arith.lh s)
:
⟪x, h.nth hx⟫ ∈ s
theorem
LO.Arith.Seq.nth_uniq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : LO.Arith.Seq s)
{x : V}
{y : V}
(hx : x < LO.Arith.lh s)
(hy : ⟪x, y⟫ ∈ s)
:
y = h.nth hx
@[simp]
theorem
LO.Arith.Seq.nth_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : LO.Arith.Seq s)
{x : V}
(hx : x < LO.Arith.lh s)
:
h.nth hx < s
theorem
LO.Arith.Seq.lh_eq_of
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(H : LO.Arith.Seq s)
{l : V}
(h : LO.Arith.domain s = LO.Arith.under l)
:
LO.Arith.lh s = l
theorem
LO.Arith.Seq.lt_lh_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : LO.Arith.Seq s)
{i : V}
:
i < LO.Arith.lh s ↔ i ∈ LO.Arith.domain s
theorem
LO.Arith.Seq.lt_lh_of_mem
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : LO.Arith.Seq s)
{i : V}
{x : V}
(hix : ⟪i, x⟫ ∈ s)
:
i < LO.Arith.lh s
Equations
- s ⁀' x = insert ⟪LO.Arith.lh s, x⟫ s
Instances For
def
LO.Arith.znth_existsUnique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(i : V)
:
∃! x : V, (LO.Arith.Seq s ∧ i < LO.Arith.lh s → ⟪i, x⟫ ∈ s) ∧ (¬(LO.Arith.Seq s ∧ i < LO.Arith.lh s) → x = 0)
Equations
- ⋯ = ⋯
Instances For
Equations
- LO.Arith.znth s i = Classical.choose! ⋯
Instances For
theorem
LO.Arith.Seq.znth
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
{i : V}
(h : LO.Arith.Seq s)
(hi : i < LO.Arith.lh s)
:
⟪i, LO.Arith.znth s i⟫ ∈ s
theorem
LO.Arith.Seq.znth_eq_of_mem
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{x : V}
{s : V}
{i : V}
(h : LO.Arith.Seq s)
(hi : ⟪i, x⟫ ∈ s)
:
LO.Arith.znth s i = x
theorem
LO.Arith.znth_prop_not
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
{i : V}
(h : ¬LO.Arith.Seq s ∨ LO.Arith.lh s ≤ i)
:
LO.Arith.znth s i = 0
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.znth_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₂ LO.Arith.znth via LO.FirstOrder.Arith.znthDef
@[simp]
theorem
LO.Arith.eval_znthDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.znthDef) ↔ v 0 = LO.Arith.znth (v 1) (v 2)
instance
LO.Arith.znth_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₂ LO.Arith.znth
Equations
- ⋯ = ⋯
instance
LO.Arith.znth_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₂ LO.Arith.znth
Equations
- ⋯ = ⋯
Equations
- LO.Arith.«term_⁀'_» = Lean.ParserDescr.trailingNode `LO.Arith.term_⁀'_ 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⁀' ") (Lean.ParserDescr.cat `term 67))
Instances For
@[simp]
@[simp]
theorem
LO.Arith.Seq.isempty_of_lh_eq_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(Hs : LO.Arith.Seq s)
(h : LO.Arith.lh s = 0)
:
@[simp]
theorem
LO.Arith.Seq.lt_seqCons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(hs : LO.Arith.Seq s)
(x : V)
:
@[simp]
theorem
LO.Arith.Seq.mem_seqCons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(x : V)
:
⟪LO.Arith.lh s, x⟫ ∈ s ⁀' x
theorem
LO.Arith.Seq.seqCons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(h : LO.Arith.Seq s)
(x : V)
:
LO.Arith.Seq (s ⁀' x)
@[simp]
theorem
LO.Arith.Seq.lh_seqCons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
{s : V}
(h : LO.Arith.Seq s)
:
LO.Arith.lh (s ⁀' x) = LO.Arith.lh s + 1
theorem
LO.Arith.mem_seqCons_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{i : V}
{x : V}
{z : V}
{s : V}
:
@[simp]
theorem
LO.Arith.lh_mem_seqCons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(z : V)
:
⟪LO.Arith.lh s, z⟫ ∈ s ⁀' z
@[simp]
theorem
LO.Arith.lh_mem_seqCons_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
{x : V}
{z : V}
(H : LO.Arith.Seq s)
:
⟪LO.Arith.lh s, x⟫ ∈ s ⁀' z ↔ x = z
theorem
LO.Arith.Seq.mem_seqCons_iff_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{i : V}
{s : V}
{x : V}
{z : V}
(hi : i < LO.Arith.lh s)
:
@[simp]
theorem
LO.Arith.lh_not_mem
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(Ss : LO.Arith.Seq s)
(x : V)
:
⟪LO.Arith.lh s, x⟫ ∉ s
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.seqCons_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₂ LO.Arith.seqCons via LO.FirstOrder.Arith.seqConsDef
@[simp]
theorem
LO.Arith.seqCons_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.seqConsDef) ↔ v 0 = v 1 ⁀' v 2
instance
LO.Arith.seqCons_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₂ LO.Arith.seqCons
Equations
- ⋯ = ⋯
instance
LO.Arith.seqCons_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₂ LO.Arith.seqCons
Equations
- ⋯ = ⋯
theorem
LO.Arith.Seq.restr
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(H : LO.Arith.Seq s)
{i : V}
(hi : i ≤ LO.Arith.lh s)
:
LO.Arith.Seq (LO.Arith.restr s (LO.Arith.under i))
theorem
LO.Arith.Seq.restr_lh
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
(H : LO.Arith.Seq s)
{i : V}
(hi : i ≤ LO.Arith.lh s)
:
LO.Arith.lh (LO.Arith.restr s (LO.Arith.under i)) = i
theorem
LO.Arith.domain_bitRemove_of_isMapping_of_mem
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{x : V}
{y : V}
{s : V}
(hs : LO.Arith.IsMapping s)
(hxy : ⟪x, y⟫ ∈ s)
:
LO.Arith.domain (LO.Arith.bitRemove ⟪x, y⟫ s) = LO.Arith.bitRemove x (LO.Arith.domain s)
theorem
LO.Arith.Seq.eq_of_eq_of_subset
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s₁ : V}
{s₂ : V}
(H₁ : LO.Arith.Seq s₁)
(H₂ : LO.Arith.Seq s₂)
(hl : LO.Arith.lh s₁ = LO.Arith.lh s₂)
(h : s₁ ⊆ s₂)
:
s₁ = s₂
theorem
LO.Arith.subset_pair
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
{t : V}
(h : ∀ (i x : V), ⟪i, x⟫ ∈ s → ⟪i, x⟫ ∈ t)
:
s ⊆ t
theorem
LO.Arith.Seq.lh_ext
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s₁ : V}
{s₂ : V}
(H₁ : LO.Arith.Seq s₁)
(H₂ : LO.Arith.Seq s₂)
(h : LO.Arith.lh s₁ = LO.Arith.lh s₂)
(H : ∀ (i x₁ x₂ : V), ⟪i, x₁⟫ ∈ s₁ → ⟪i, x₂⟫ ∈ s₂ → x₁ = x₂)
:
s₁ = s₂
@[simp]
theorem
LO.Arith.Seq.seqCons_ext
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{a₁ : V}
{a₂ : V}
{s₁ : V}
{s₂ : V}
(H₁ : LO.Arith.Seq s₁)
(H₂ : LO.Arith.Seq s₂)
:
TODO: move to Lemmata.lean
theorem
LO.Arith.Seq.cases_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
:
LO.Arith.Seq s ↔ s = ∅ ∨ ∃ (x : V) (s' : V), LO.Arith.Seq s' ∧ s = s' ⁀' x
theorem
LO.Arith.Seq.cases
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{s : V}
:
LO.Arith.Seq s → s = ∅ ∨ ∃ (x : V) (s' : V), LO.Arith.Seq s' ∧ s = s' ⁀' x
Alias of the forward direction of LO.Arith.Seq.cases_iff
.
theorem
LO.Arith.seq_induction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
{P : V → Prop}
(hP : { Γ := Γ, rank := 1 }-Predicate P)
(hnil : P ∅)
(hcons : ∀ (s x : V), LO.Arith.Seq s → P s → P (s ⁀' x))
{s : V}
:
LO.Arith.Seq s → P s
!⟦x, y, z, ...⟧
notation for Seq
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.Arith.singleton_seq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
:
LO.Arith.Seq !⟦x⟧
@[simp]
theorem
LO.Arith.doubleton_seq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(y : V)
:
LO.Arith.Seq !⟦x, y⟧
@[simp]
theorem
LO.Arith.mem_singleton_seq_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(y : V)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.mkSeq₁_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ fun (x : V) => !⟦x⟧ via LO.FirstOrder.Arith.mkSeq₁Def
@[simp]
instance
LO.Arith.mkSeq₁_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ fun (x : V) => !⟦x⟧
Equations
- ⋯ = ⋯
instance
LO.Arith.mkSeq₁_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.FirstOrder.Arith.HierarchySymbol)
:
Γ-Function₁ fun (x : V) => !⟦x⟧
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.mkSeq₂_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ fun (x y : V) => !⟦x, y⟧ via LO.FirstOrder.Arith.mkSeq₂Def
@[simp]
theorem
LO.Arith.eval_mkSeq₂Def
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.mkSeq₂Def) ↔ v 0 = !⟦v 1, v 2⟧
instance
LO.Arith.mkSeq₂_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ fun (x y : V) => !⟦x, y⟧
Equations
- ⋯ = ⋯
instance
LO.Arith.mkSeq₂_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
{ Γ := Γ, rank := m + 1 }-Function₂ fun (x y : V) => !⟦x, y⟧
Equations
- ⋯ = ⋯
theorem
LO.Arith.sigmaOne_skolem_seq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{R : V → V → Prop}
(hP : 𝚺₁-Relation R)
{l : V}
(H : ∀ x < l, ∃ (y : V), R x y)
:
∃ (s : V), LO.Arith.Seq s ∧ LO.Arith.lh s = l ∧ ∀ (i x : V), ⟪i, x⟫ ∈ s → R i x
theorem
LO.Arith.sigmaOne_skolem_seq!
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{R : V → V → Prop}
(hP : 𝚺₁-Relation R)
{l : V}
(H : ∀ x < l, ∃! y : V, R x y)
:
∃! s : V, LO.Arith.Seq s ∧ LO.Arith.lh s = l ∧ ∀ (i x : V), ⟪i, x⟫ ∈ s → R i x
Equations
- LO.Arith.vecToSeq x_2 = ∅
- LO.Arith.vecToSeq v = (LO.Arith.vecToSeq fun (x : Fin n) => v x.castSucc) ⁀' v (Fin.last n)
Instances For
@[simp]
theorem
LO.Arith.vecToSeq_nil
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
LO.Arith.vecToSeq ![] = ∅
@[simp]
theorem
LO.Arith.vecToSeq_vecCons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(v : Fin n → V)
(a : V)
:
LO.Arith.vecToSeq (v <: a) = LO.Arith.vecToSeq v ⁀' a
@[simp]
theorem
LO.Arith.vecToSeq_seq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(v : Fin n → V)
:
@[simp]
theorem
LO.Arith.lh_vecToSeq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(v : Fin n → V)
:
LO.Arith.lh (LO.Arith.vecToSeq v) = ↑n
theorem
LO.Arith.mem_vectoSeq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(v : Fin n → V)
(i : Fin n)
:
⟪↑↑i, v i⟫ ∈ LO.Arith.vecToSeq v
theorem
LO.Arith.order_ball_induction_sigma1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{f : V → V → V}
(hf : 𝚺₁-Function₂ f)
{P : V → V → Prop}
(hP : 𝚺₁-Relation P)
(ind : ∀ (x y : V), (∀ x' < x, ∀ y' ≤ f x y, P x' y') → P x y)
(x : V)
(y : V)
:
P x y
theorem
LO.Arith.order_ball_induction_sigma1'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{f : V → V}
(hf : 𝚺₁-Function₁ f)
{P : V → V → Prop}
(hP : 𝚺₁-Relation P)
(ind : ∀ (x y : V), (∀ x' < x, ∀ y' ≤ f y, P x' y') → P x y)
(x : V)
(y : V)
:
P x y
theorem
LO.Arith.order_ball_induction₂_sigma1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{fy : V → V → V → V}
{fz : V → V → V → V}
(hfy : 𝚺₁-Function₃ fy)
(hfz : 𝚺₁-Function₃ fz)
{P : V → V → V → Prop}
(hP : 𝚺₁-Relation₃ P)
(ind : ∀ (x y z : V), (∀ x' < x, ∀ y' ≤ fy x y z, ∀ z' ≤ fz x y z, P x' y' z') → P x y z)
(x : V)
(y : V)
(z : V)
:
P x y z
theorem
LO.Arith.order_ball_induction₃_sigma1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{fy : V → V → V → V → V}
{fz : V → V → V → V → V}
{fw : V → V → V → V → V}
(hfy : 𝚺₁-Function₄ fy)
(hfz : 𝚺₁-Function₄ fz)
(hfw : 𝚺₁-Function₄ fw)
{P : V → V → V → V → Prop}
(hP : 𝚺₁-Relation₄ P)
(ind : ∀ (x y z w : V), (∀ x' < x, ∀ y' ≤ fy x y z w, ∀ z' ≤ fz x y z w, ∀ w' ≤ fw x y z w, P x' y' z' w') → P x y z w)
(x : V)
(y : V)
(z : V)
(w : V)
:
P x y z w