flag_le_ker_coord_iff — Mathlib

English

For any k and l, F_k ≤ ker(coord_l) if and only if k ≤ l.castSucc.

Русский

При любом k и l: F_k ≤ ker(coord_l) тогда и только тогда, когда k ≤ l.castSucc.

LaTeX

$$$F_k \le \ker(\mathrm{coord}_l) \quad\Leftrightarrow\quad k \le l^{\uparrow}$$$

Lean4

@[simp]
theorem flag_le_ker_coord_iff [Nontrivial R] (b : Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n} :
    b.flag k ≤ LinearMap.ker (b.coord l) ↔ k ≤ l.castSucc := by
  simp [flag_le_iff, Finsupp.single_apply_eq_zero, imp_false, imp_not_comm]

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