isMaxChain_range_flag

Mathlib.LinearAlgebra.Basis.Flag

URI: https://scilib.ai/kg/mathlib#Module.Basis.isMaxChain_range_flag

English

The range of the flag is a maximal chain with respect to inclusion.

Русский

Диапазон флага образует максимальную цепь по включению.

LaTeX

$$IsMaxChain (≤) (range (b.flag))$$

Lean4

theorem isMaxChain_range_flag (b : Basis (Fin n) K V) : IsMaxChain (· ≤ ·) (range b.flag) :=
  b.toFlag.maxChain

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru