flag_covBy

Mathlib.LinearAlgebra.Basis.Flag

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

← MathLib Explorer

English

For each i, F_i.castSucc CovBy F_i.succ; i.e., F_i.castSucc is covered by F_i.succ.

Русский

Для каждого i: F_i.castSucc покрывается F_i.succ; т.е. они соседствуют в порядке вложенности.

LaTeX

$$F_i.castSucc covBy F_i.succ$$

Lean4

theorem flag_covBy (b : Basis (Fin n) K V) (i : Fin n) : b.flag i.castSucc ⋖ b.flag i.succ :=
  by
  rw [flag_succ]
  apply covBy_span_singleton_sup
  simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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