flag_le_iff — Mathlib

English

For a basis b of Fin n, the flag k is contained in p if and only if every basis vector with index i satisfying i.castSucc < k lies in p.

Русский

Для базиса b над Fin n условие, что флаг k ⊆ p эквивалентно тому, что каждый вектор базиса b с индексом i, удовлетворяющим i.castSucc < k, принадлежит p.

LaTeX

$$$ b.flag k \le p \iff \forall i : Fin n, i.castSucc < k \rightarrow b i \in p $$$

Lean4

theorem flag_le_iff (b : Basis (Fin n) R M) {k p} : b.flag k ≤ p ↔ ∀ i : Fin n, i.castSucc < k → b i ∈ p :=
  span_le.trans forall_mem_image

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