flag_strictMono

Mathlib.LinearAlgebra.Basis.Flag

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

← MathLib Explorer

English

If the base ring is nontrivial, the flag is strictly increasing: i < j implies F_i ⊊ F_j.

Русский

Если кольцо не тождественно нулю, флаг строго возрастает: i < j означает F_i ⊊ F_j.

LaTeX

$$$i < j \implies F_i \subsetneq F_j$$$

Lean4

@[mono]
theorem flag_strictMono [Nontrivial R] (b : Basis (Fin n) R M) : StrictMono b.flag :=
  Fin.strictMono_iff_lt_succ.2 fun _ ↦ by simp [flag_succ]

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

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

Разделы

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

Аффилиация

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