efixedPoint_isFixedPt' — Mathlib

English

In the forward-invariant setting, efixedPoint' is a fixed point of f.

Русский

В условиях инвариантности efixedPoint' является фиксированной точкой f.

LaTeX

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

Lean4

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

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