flag_mono

Mathlib.LinearAlgebra.Basis.Flag

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

English

The flag function is monotone with respect to index: if i ≤ j then F_i ⊆ F_j.

Русский

Функция флага монотонна по отношению к индексу: если i ≤ j, то F_i ⊆ F_j.

LaTeX

$$$\text{If } i \le j, \ F_i \subseteq F_j.$$$

Lean4

@[mono]
theorem flag_mono (b : Basis (Fin n) R M) : Monotone b.flag :=
  Fin.monotone_iff_le_succ.2 fun k ↦ by rw [flag_succ]; exact le_sup_right

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

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

Разделы

Аффилиация

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