succAbove_le_succAbove_iff

Mathlib.Order.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.succAbove_le_succAbove_iff

English

For any p, the relation i ≤ j is equivalent to succAbove p i ≤ succAbove p j.

Русский

Для любого p отношение i ≤ j эквивалентно succAbove p i ≤ succAbove p j.

LaTeX

$$$\forall p:\mathrm{Fin}(n+1),\; \text{succAbove }p\; i \le \text{succAbove }p\; j \iff i \le j$$$

Lean4

@[simp]
theorem succAbove_le_succAbove_iff : succAbove p i ≤ succAbove p j ↔ i ≤ j :=
  (strictMono_succAbove p).le_iff_le

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

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

Разделы

Аффилиация

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