flag_lt_flag

Mathlib.LinearAlgebra.Basis.Flag

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

English

If i < j (with a nontrivial base ring), then F_i < F_j.

Русский

Если i < j и база не тривиальна, то F_i < F_j.

LaTeX

$$$i < j \Rightarrow F_i < F_j$$$

Lean4

@[gcongr]
theorem flag_lt_flag [Nontrivial R] (hij : i < j) : b.flag i < b.flag j :=
  flag_strictMono _ hij

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

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

Разделы

Аффилиация

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