monotone — Mathlib

English

If i<j and both below o, then f(i) ≤ f(j) under the default choice of cases (monotone nondecreasing in the index when i=j or i<j).

Русский

Если i<j и оба меньше o, то f(i) ≤ f(j) в условиях монотонности функции f.

LaTeX

$$$$\forall i

Lean4

protected theorem monotone (hf : IsFundamentalSequence a o f) {i j : Ordinal} (hi : i < o) (hj : j < o) (hij : i ≤ j) :
    f i hi ≤ f j hj := by
  rcases lt_or_eq_of_le hij with (hij | rfl)
  · exact (hf.2.1 hi hj hij).le
  · rfl

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