Documentation

Foundation.FirstOrder.ISigma1.HFS.Seq

Sequence #

source
def LO.ISigma1.Seq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
Prop
Equations
Instances For
source
def LO.ISigma1.Seq.isMapping {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : Seq s) :
IsMapping s
Equations
  • ⋯ = ⋯
source
def LO.FirstOrder.Arithmetic.seqDef :
𝚺₀.Semisentence 1
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.ISigma1.seq_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₀-Predicate Seq via FirstOrder.Arithmetic.seqDef
source
@[simp]
theorem LO.ISigma1.seq_defined_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 1 → V) :
V ⊧/v ↑FirstOrder.Arithmetic.seqDef ↔ Seq (v 0)
source
instance LO.ISigma1.seq_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₀-Predicate Seq
source
instance LO.ISigma1.seq_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : FirstOrder.Arithmetic.HierarchySymbol) :
ℌ-Predicate Seq
source
def LO.ISigma1.«first_order_formula:Seq_» :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.ISigma1.lh_exists_uniq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
∃! l : V, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
source
noncomputable def LO.ISigma1.lh {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
V
Equations
Instances For
source
theorem LO.ISigma1.lh_prop {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
(Seq s → domain s = under (lh s)) ∧ (¬Seq s → lh s = 0)
source
theorem LO.ISigma1.lh_prop_of_not_seq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : ¬Seq s) :
lh s = 0
source
theorem LO.ISigma1.Seq.domain_eq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : Seq s) :
domain s = under (lh s)
source
@[simp]
theorem LO.ISigma1.lh_bound {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
lh s ≤ 2 * s
source
def LO.FirstOrder.Arithmetic.lhDef :
𝚺₀.Semisentence 2
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.ISigma1.lh_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₀-Function₁ lh via FirstOrder.Arithmetic.lhDef
source
@[simp]
theorem LO.ISigma1.lh_defined_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) :
V ⊧/v ↑FirstOrder.Arithmetic.lhDef ↔ v 0 = lh (v 1)
source
instance LO.ISigma1.lh_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₀-Function₁ lh
source
instance LO.ISigma1.lh_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : FirstOrder.Arithmetic.HierarchySymbol) :
ℌ-Function₁ lh
source
instance LO.ISigma1.instBounded₁Lh {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
FirstOrder.Arithmetic.Bounded₁ lh
source
theorem LO.ISigma1.Seq.exists {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : Seq s) {x : V} (hx : x < lh s) :
∃ (y : V), ⟪x, y⟫ ∈ s
source
theorem LO.ISigma1.Seq.nth_exists_uniq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : Seq s) {x : V} (hx : x < lh s) :
∃! y : V, ⟪x, y⟫ ∈ s
source
noncomputable def LO.ISigma1.Seq.nth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : Seq s) {x : V} (hx : x < lh s) :
V
Equations
source
@[simp]
theorem LO.ISigma1.Seq.nth_mem {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : Seq s) {x : V} (hx : x < lh s) :
⟪x, h.nth hx⟫ ∈ s
source
theorem LO.ISigma1.Seq.nth_uniq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : Seq s) {x y : V} (hx : x < lh s) (hy : ⟪x, y⟫ ∈ s) :
y = h.nth hx
source
@[simp]
theorem LO.ISigma1.Seq.nth_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : Seq s) {x : V} (hx : x < lh s) :
h.nth hx < s
source
theorem LO.ISigma1.Seq.lh_eq_of {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (H : Seq s) {l : V} (h : domain s = under l) :
lh s = l
source
theorem LO.ISigma1.Seq.lt_lh_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : Seq s) {i : V} :
i < lh s ↔ i ∈ domain s
source
theorem LO.ISigma1.Seq.lt_lh_of_mem {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : Seq s) {i x : V} (hix : ⟪i, x⟫ ∈ s) :
i < lh s
source
noncomputable def LO.ISigma1.seqCons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s x : V) :
V
Equations
Instances For
source
def LO.ISigma1.znth_existsUnique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s i : V) :
∃! x : V, (Seq s ∧ i < lh s → ⟪i, x⟫ ∈ s) ∧ (¬(Seq s ∧ i < lh s) → x = 0)
Equations
  • ⋯ = ⋯
source
noncomputable def LO.ISigma1.znth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s i : V) :
V
Equations
Instances For
source
theorem LO.ISigma1.Seq.znth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s i : V} (h : Seq s) (hi : i < lh s) :
⟪i, znth s i⟫ ∈ s
source
theorem LO.ISigma1.Seq.znth_eq_of_mem {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x s i : V} (h : Seq s) (hi : ⟪i, x⟫ ∈ s) :
znth s i = x
source
theorem LO.ISigma1.znth_prop_not {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s i : V} (h : ¬Seq s ∨ lh s ≤ i) :
znth s i = 0
source
def LO.FirstOrder.Arithmetic.znthDef :
𝚺₀.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.ISigma1.znth_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₀-Function₂ znth via FirstOrder.Arithmetic.znthDef
source
@[simp]
theorem LO.ISigma1.eval_znthDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :
V ⊧/v ↑FirstOrder.Arithmetic.znthDef ↔ v 0 = znth (v 1) (v 2)
source
instance LO.ISigma1.znth_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₀-Function₂ znth
source
instance LO.ISigma1.znth_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : FirstOrder.Arithmetic.HierarchySymbol) :
ℌ-Function₂ znth
source
def LO.ISigma1.«term_⁀'_» :
Lean.TrailingParserDescr
Equations
source
@[simp]
theorem LO.ISigma1.seq_empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
Seq ∅
source
@[simp]
theorem LO.ISigma1.lh_empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
lh ∅ = 0
source
theorem LO.ISigma1.Seq.isempty_of_lh_eq_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (Hs : Seq s) (h : lh s = 0) :
s = ∅
source
@[simp]
theorem LO.ISigma1.Seq.subset_seqCons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s x : V) :
s ⊆ s ⁀' x
source
theorem LO.ISigma1.Seq.lt_seqCons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (hs : Seq s) (x : V) :
s < s ⁀' x
source
@[simp]
theorem LO.ISigma1.Seq.mem_seqCons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s x : V) :
⟪lh s, x⟫ ∈ s ⁀' x
source
theorem LO.ISigma1.Seq.seqCons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : Seq s) (x : V) :
Seq (s ⁀' x)
source
@[simp]
theorem LO.ISigma1.Seq.lh_seqCons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) {s : V} (h : Seq s) :
lh (s ⁀' x) = lh s + 1
source
theorem LO.ISigma1.mem_seqCons_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i x z s : V} :
⟪i, x⟫ ∈ s ⁀' z ↔ i = lh s ∧ x = z ∨ ⟪i, x⟫ ∈ s
source
@[simp]
theorem LO.ISigma1.lh_mem_seqCons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s z : V) :
⟪lh s, z⟫ ∈ s ⁀' z
source
@[simp]
theorem LO.ISigma1.lh_mem_seqCons_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s x z : V} (H : Seq s) :
⟪lh s, x⟫ ∈ s ⁀' z ↔ x = z
source
theorem LO.ISigma1.Seq.mem_seqCons_iff_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i s x z : V} (hi : i < lh s) :
⟪i, x⟫ ∈ s ⁀' z ↔ ⟪i, x⟫ ∈ s
source
@[simp]
theorem LO.ISigma1.lh_not_mem {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (Ss : Seq s) (x : V) :
⟪lh s, x⟫ ∉ s
source
theorem LO.ISigma1.seqCons_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (t x s : V) :
t = s ⁀' x ↔ ∃ l ≤ 2 * s, l = lh s ∧ ∃ p ≤ (2 * s + x + 1) ^ 2, p = ⟪l, x⟫ ∧ t = insert p s
source
def LO.FirstOrder.Arithmetic.seqConsDef :
𝚺₀.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.ISigma1.seqCons_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₀-Function₂ seqCons via FirstOrder.Arithmetic.seqConsDef
source
@[simp]
theorem LO.ISigma1.seqCons_defined_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :
V ⊧/v ↑FirstOrder.Arithmetic.seqConsDef ↔ v 0 = v 1 ⁀' v 2
source
instance LO.ISigma1.seqCons_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₀-Function₂ seqCons
source
instance LO.ISigma1.seqCons_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : FirstOrder.Arithmetic.HierarchySymbol) :
ℌ-Function₂ seqCons
source
@[simp]
theorem LO.ISigma1.natCast_empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
↑∅ = ∅
source
theorem LO.ISigma1.seqCons_absolute {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s a : ℕ) :
↑(s ⁀' a) = ↑s ⁀' ↑a
source
theorem LO.ISigma1.Seq.restr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (H : Seq s) {i : V} (hi : i ≤ lh s) :
Seq (ISigma1.restr s (under i))
source
theorem LO.ISigma1.Seq.restr_lh {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (H : Seq s) {i : V} (hi : i ≤ lh s) :
lh (ISigma1.restr s (under i)) = i
source
theorem LO.ISigma1.domain_bitRemove_of_isMapping_of_mem {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x y s : V} (hs : IsMapping s) (hxy : ⟪x, y⟫ ∈ s) :
domain (bitRemove ⟪x, y⟫ s) = bitRemove x (domain s)
source
theorem LO.ISigma1.Seq.eq_of_eq_of_subset {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s₁ s₂ : V} (H₁ : Seq s₁) (H₂ : Seq s₂) (hl : lh s₁ = lh s₂) (h : s₁ ⊆ s₂) :
s₁ = s₂
source
theorem LO.ISigma1.subset_pair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s t : V} (h : ∀ (i x : V), ⟪i, x⟫ ∈ s → ⟪i, x⟫ ∈ t) :
s ⊆ t
source
theorem LO.ISigma1.Seq.lh_ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s₁ s₂ : V} (H₁ : Seq s₁) (H₂ : Seq s₂) (h : lh s₁ = lh s₂) (H : ∀ (i x₁ x₂ : V), ⟪i, x₁⟫ ∈ s₁ → ⟪i, x₂⟫ ∈ s₂ → x₁ = x₂) :
s₁ = s₂
source
@[simp]
theorem LO.ISigma1.Seq.seqCons_ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a₁ a₂ s₁ s₂ : V} (H₁ : Seq s₁) (H₂ : Seq s₂) :
s₁ ⁀' a₁ = s₂ ⁀' a₂ ↔ a₁ = a₂ ∧ s₁ = s₂
source
theorem LO.ISigma1.ne_zero_iff_one_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} :
a ≠ 0 ↔ 1 ≤ a

TODO: move to Lemmata.lean

source
theorem LO.ISigma1.Seq.cases_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} :
Seq s ↔ s = ∅ ∨ ∃ (x : V) (s' : V), Seq s' ∧ s = s' ⁀' x
source
theorem LO.ISigma1.Seq.cases {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} :
Seq s → s = ∅ ∨ ∃ (x : V) (s' : V), Seq s' ∧ s = s' ⁀' x

Alias of the forward direction of LO.ISigma1.Seq.cases_iff.

source
theorem LO.ISigma1.seq_induction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hnil : P ∅) (hcons : ∀ (s x : V), Seq s → P s → P (s ⁀' x)) {s : V} :
Seq s → P s
source
def LO.ISigma1.«term!⟦_⟧» :
Lean.ParserDescr

!⟦x, y, z, ...⟧ notation for Seq

Equations
  • One or more equations did not get rendered due to their size.
source
def LO.ISigma1.vecConsUnexpander :
Lean.PrettyPrinter.Unexpander
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem LO.ISigma1.singleton_seq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
Seq !⟦x⟧
source
@[simp]
theorem LO.ISigma1.doubleton_seq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
Seq !⟦x, y⟧
source
@[simp]
theorem LO.ISigma1.mem_singleton_seq_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
⟪0, x⟫ ∈ !⟦y⟧ ↔ x = y
source
def LO.FirstOrder.Arithmetic.mkSeq₁Def :
𝚺₀.Semisentence 2
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.ISigma1.mkSeq₁_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₀-Function₁ fun (x : V) => !⟦x⟧ via FirstOrder.Arithmetic.mkSeq₁Def
source
@[simp]
theorem LO.ISigma1.eval_mkSeq₁Def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) :
V ⊧/v ↑FirstOrder.Arithmetic.mkSeq₁Def ↔ v 0 = !⟦v 1⟧
source
instance LO.ISigma1.mkSeq₁_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₀-Function₁ fun (x : V) => !⟦x⟧
source
instance LO.ISigma1.mkSeq₁_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : FirstOrder.Arithmetic.HierarchySymbol) :
Γ-Function₁ fun (x : V) => !⟦x⟧
source
def LO.FirstOrder.Arithmetic.mkSeq₂Def :
𝚺₁.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.ISigma1.mkSeq₂_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₁-Function₂ fun (x y : V) => !⟦x, y⟧ via FirstOrder.Arithmetic.mkSeq₂Def
source
@[simp]
theorem LO.ISigma1.eval_mkSeq₂Def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :
V ⊧/v ↑FirstOrder.Arithmetic.mkSeq₂Def ↔ v 0 = !⟦v 1, v 2⟧
source
instance LO.ISigma1.mkSeq₂_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₁-Function₂ fun (x y : V) => !⟦x, y⟧
source
instance LO.ISigma1.mkSeq₂_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ℕ) :
{ Γ := Γ, rank := m + 1 }-Function₂ fun (x y : V) => !⟦x, y⟧
source
theorem LO.ISigma1.sigmaOne_skolem_seq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {R : V → V → Prop} (hP : 𝚺₁-Relation R) {l : V} (H : ∀ x < l, ∃ (y : V), R x y) :
∃ (s : V), Seq s ∧ lh s = l ∧ ∀ (i x : V), ⟪i, x⟫ ∈ s → R i x
source
theorem LO.ISigma1.sigmaOne_skolem_seq! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {R : V → V → Prop} (hP : 𝚺₁-Relation R) {l : V} (H : ∀ x < l, ∃! y : V, R x y) :
∃! s : V, Seq s ∧ lh s = l ∧ ∀ (i x : V), ⟪i, x⟫ ∈ s → R i x
source
noncomputable def LO.ISigma1.vecToSeq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} :
(Fin n → V) → V
Equations
source
@[simp]
theorem LO.ISigma1.vecToSeq_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
vecToSeq ![] = ∅
source
@[simp]
theorem LO.ISigma1.vecToSeq_vecCons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin n → V) (a : V) :
vecToSeq (v <: a) = vecToSeq v ⁀' a
source
@[simp]
theorem LO.ISigma1.vecToSeq_seq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin n → V) :
Seq (vecToSeq v)
source
@[simp]
theorem LO.ISigma1.lh_vecToSeq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin n → V) :
lh (vecToSeq v) = ↑n
source
theorem LO.ISigma1.mem_vectoSeq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin n → V) (i : Fin n) :
⟪↑↑i, v i⟫ ∈ vecToSeq v