efixedPoint — Mathlib

English

The efixedPoint' value lies in the set s.

Русский

Значение efixedPoint' принадлежит множеству s.

LaTeX

$$$ efixedPoint'\, f\, hsc\, hsf\, hf\, x\, hxs\, hx \in s $$$

Lean4

/-- Let `x` be a point of a complete emetric space. Suppose that `f` is a contracting map,
and `edist x (f x) ≠ ∞`. Then `efixedPoint` is the unique fixed point of `f`
in `EMetric.ball x ∞`. -/
noncomputable def efixedPoint (hf : ContractingWith K f) (x : α) (hx : edist x (f x) ≠ ∞) : α :=
  Classical.choose <| hf.exists_fixedPoint x hx

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