efixedPoint_mem' — Mathlib

English

The value efixedPoint' is a fixed point of f restricted to s.

Русский

Значение efixedPoint' является фиксированной точкой f на s.

LaTeX

$$$ IsFixedPt\, f\, (efixedPoint'\, f\, hsc\, hsf) $$$

Lean4

theorem efixedPoint_mem' {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) ≠ ∞) :
    efixedPoint' f hsc hsf hf x hxs hx ∈ s :=
  (Classical.choose_spec <| hf.exists_fixedPoint' hsc hsf hxs hx).1

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