le_of_isLE

Mathlib.CategoryTheory.Triangulated.TStructure.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Triangulated.TStructure.le_of_isLE

English

If t.IsLE X n holds, then t.le n X holds.

Русский

Если t.IsLE X n, то t.le n X.

LaTeX

$$$[t.IsLE X n] \\Rightarrow t.le n X$$$

Lean4

theorem le_of_isLE (X : C) (n : ℤ) [t.IsLE X n] : t.le n X :=
  IsLE.le

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

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

Разделы

Аффилиация

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