self_mem_flag_iff — Mathlib

English

For a basis b and indices i, k, the membership b(i) ∈ F_k is equivalent to i.castSucc < k.

Русский

Для базиса b и индексов i, k верно равенство: b(i) принадлежит F_k тогда и только тогда, когда i.castSucc < k.

LaTeX

$$$b_i \in F_k \iff i^{\uparrow} < k$$$

Lean4

@[simp]
theorem self_mem_flag_iff [Nontrivial R] (b : Basis (Fin n) R M) {i : Fin n} {k : Fin (n + 1)} :
    b i ∈ b.flag k ↔ i.castSucc < k :=
  b.self_mem_span_image

Похожие утверждения