le_prevFixed — Mathlib

English

If hx is a proof that f(x) ≤ x, then for any y in fixedPoints f with y ≤ x, y ≤ prevFixed(x, hx).

Русский

Если есть доказательство f(x) ≤ x, то для любого y из фиксированных точек f с y ≤ x, выполняется y ≤ prevFixed(x, hx).

LaTeX

$$$(hx) \Rightarrow (y \le x) \Rightarrow y \le \mathrm{prevFixed}(x, hx).$$$

Lean4

theorem le_prevFixed {x : α} (hx : f x ≤ x) {y : fixedPoints f} (h : ↑y ≤ x) : y ≤ f.prevFixed x hx :=
  (f.le_prevFixed_iff hx).2 h

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