flag_wcovBy

Mathlib.LinearAlgebra.Basis.Flag

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

English

F_i.castSucc is weakly covBy F_i.succ.

Русский

F_i.castSucc слабопокрывает F_i.succ.

LaTeX

$$F_i.castSucc wcovBy F_i.succ$$

Lean4

theorem flag_wcovBy (b : Basis (Fin n) K V) (i : Fin n) : b.flag i.castSucc ⩿ b.flag i.succ :=
  (b.flag_covBy i).wcovBy

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

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

Разделы

Аффилиация

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