succFn_le_of_lt — Mathlib

English

Locally finite linear orders carry IsPredArchimedean; hence IsSuccArchimedean as well by duality.

Русский

Локально конечные линейные порядки удовлетворяют IsPredArchimedean; следовательно, через дуальность и IsSuccArchimedean.

LaTeX

$$$[LocallyFiniteOrder(ι)] \\Rightarrow IsPredArchimedean(ι) \\Rightarrow IsSuccArchimedean(ι)$$$

Lean4

theorem succFn_le_of_lt (i j : ι) (hij : i < j) : succFn i ≤ j :=
  by
  have h := succFn_spec i
  rw [IsGLB, IsGreatest, mem_lowerBounds] at h
  exact h.1 j hij

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