edist_efixedPoint_lt_top — Mathlib

English

The distance to efixedPoint is strictly less than top (finite).

Русский

Расстояние до efixedPoint строго меньше бесконечности.

LaTeX

$$$ edist(x, efixedPoint\, f\, hf\, x\, hx) < \infty $$$

Lean4

theorem edist_efixedPoint_lt_top (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ∞) :
    edist x (efixedPoint f hf x hx) < ∞ :=
  (hf.edist_efixedPoint_le hx).trans_lt (ENNReal.mul_ne_top hx <| ENNReal.inv_ne_top.2 hf.one_sub_K_ne_zero).lt_top

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