le

Mathlib.AlgebraicTopology.SimplicialNerve

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SimplicialThickening.Path.le

English

In a thickened simplicial path, the left endpoint is less than or equal to the right endpoint: i ≤ j for f : Path i j.

Русский

В пути утолщённого симпликса левая конечная точка не превышает правую: i ≤ j для f : Path i j.

LaTeX

$$$$ i \le j $$$$

Lean4

theorem le {J : Type*} [LinearOrder J] {i j : J} (f : Path i j) : i ≤ j :=
  f.left_le _ f.right

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

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

Разделы

Аффилиация

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