English
Under contraction on a complete space, there exists a fixed point for the unrestricted map on the whole space.
Русский
При сжатии на полное пространство существует фиксированная точка для полного отображения.
LaTeX
$$$ \exists y, \ IsFixedPt f y \land \cdots $$$
Lean4
/-- Let `s` be a complete forward-invariant set of a self-map `f`. If `f` contracts on `s`
and `x ∈ s` satisfies `edist x (f x) ≠ ∞`, then `efixedPoint'` is the unique fixed point
of the restriction of `f` to `s ∩ EMetric.ball x ∞`. -/
noncomputable def efixedPoint' {s : Set α} (hsc : IsComplete s) (hsf : MapsTo f s s)
(hf : ContractingWith K <| hsf.restrict f s s) (x : α) (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) : α :=
Classical.choose <| hf.exists_fixedPoint' hsc hsf hxs hx
