isChain_range_flag — Mathlib

English

The range of the flag map forms a chain under inclusion; i.e., any two flag subspaces are comparable by inclusion.

Русский

Область значений флага образует цепь по включению: любые две подпространства флага сравнимы по включению.

LaTeX

$$$\operatorname{IsChain}\, (\le)\ (\operatorname{range} (b.flag)).$$$

Lean4

theorem isChain_range_flag (b : Basis (Fin n) R M) : IsChain (· ≤ ·) (range b.flag) :=
  b.flag_mono.isChain_range

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