nextFixed_le_iff — Mathlib

English

The relation x ≤ nextFixed(x) is equivalent to f.nextFixed(x) ≤ y for fixed y.

Русский

Отношение x ≤ nextFixed(x) эквивалентно f.nextFixed(x) ≤ y для фиксированного y.

LaTeX

$$$(x \le f(x)) \Rightarrow (f.nextFixed(x) \le y) \Leftrightarrow x \le y.$$$

Lean4

@[simp]
theorem nextFixed_le_iff {x : α} (hx : x ≤ f x) {y : fixedPoints f} : f.nextFixed x hx ≤ y ↔ x ≤ y :=
  ⟨fun h => (f.le_nextFixed hx).trans h, f.nextFixed_le hx⟩

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