English
Let b be a basis of a module M over a semiring R, indexed by Fin n. Denote by F_i the i-th subspace in the flag generated by b. Then for every i in Fin n, the (i+1)-st flag equals the sum of the span of the i-th basis vector with the i-th flag: F_{i+1} = span_R{b(i)} + F_i.
Русский
Пусть b — базис модуля M над полем/кольцом R, индексируемый по Fin n. Обозначим F_i как i-ую подпространство в флаге, порождаемом базисом b. Тогда для каждого i из Fin n выполнено: F_{i+1} = span_R{b(i)} + F_i.
LaTeX
$$$F_{k+1} = \operatorname{span}_R\{b_k\} + F_k$$$
Lean4
theorem flag_succ (b : Basis (Fin n) R M) (k : Fin n) : b.flag k.succ = (R ∙ b k) ⊔ b.flag k.castSucc :=
by
simp only [flag, Fin.castSucc_lt_castSucc_iff]
simp [Fin.castSucc_lt_iff_succ_le, le_iff_eq_or_lt, setOf_or, image_insert_eq, span_insert]
