le_of_lt_succFn

Mathlib.Order.SuccPred.LinearLocallyFinite

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

← MathLib Explorer

English

If j is strictly less than the bound succFn(i) for i, then j ≤ i.

Русский

Если j строго меньше bound succFn(i), то j ≤ i.

LaTeX

$$$j < \\mathrm{succFn}(i) \\Rightarrow j \\le i$$$

Lean4

theorem le_of_lt_succFn (j i : ι) (hij : j < succFn i) : j ≤ i :=
  by
  rw [lt_isGLB_iff (succFn_spec i)] at hij
  obtain ⟨k, hk_lb, hk⟩ := hij
  rw [mem_lowerBounds] at hk_lb
  exact not_lt.mp fun hi_lt_j ↦ not_le.mpr hk (hk_lb j hi_lt_j)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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