le_succFn

Mathlib.Order.SuccPred.LinearLocallyFinite

URI: https://scilib.ai/kg/mathlib#LinearLocallyFiniteOrder.le_succFn

English

For a linear locally finite order, the order is compatible with the successor function: i ≤ succ(i).

Русский

Для линейного локально конечного порядка i ≤ succ(i).

LaTeX

$$$i \\leq \\text{succFn}(i)$$$

Lean4

theorem le_succFn (i : ι) : i ≤ succFn i :=
  by
  rw [le_isGLB_iff (succFn_spec i), mem_lowerBounds]
  exact fun x hx ↦ le_of_lt hx

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

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

Разделы

Аффилиация

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