self_mem_flag — Mathlib

English

Let b be a basis of M over R. If i.castSucc < k, then the i-th basis vector b(i) lies in the k-th flag subspace F_k.

Русский

Пусть b — базис пространства M над R. Если i.castSucc < k, то в k-ом подпространстве флага содержится вектор b(i).

LaTeX

$$$b_i \in F_k \quad\text{ whenever } i^{\uparrow} < k$$$

Lean4

theorem self_mem_flag (b : Basis (Fin n) R M) {i : Fin n} {k : Fin (n + 1)} (h : i.castSucc < k) : b i ∈ b.flag k :=
  subset_span <| mem_image_of_mem _ h

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