OriginalNorm.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The fixed point property in the given norm

The public property quantifies over actual convex subsets and their selfmaps. Its nonexpansiveness condition uses the existing ambient norm. These elementary interface lemmas neither change that norm nor supply the main reflexive-space theorem; the latter is proved by the reduction and contradiction chain.

theorem OAI.ReflexiveFixedPoints.nonexpansiveOn_iff_lipschitzWith_one line 23
theorem OAI.ReflexiveFixedPoints.hasNonexpansiveFixedPointProperty_of_subsingleton line 36
Source documentation
In particular, the property includes the zero space.
```
theorem hasNonexpansiveFixedPointProperty_of_subsingleton [Subsingleton X] :
    HasNonexpansiveFixedPointProperty X := by
…
```
Mentions: OAI.ReflexiveFixedPoints.HasNonexpansiveFixedPointProperty

theorem OAI.ReflexiveFixedPoints.ambient_fixedPoint_of_property line 43

Source documentation

An ambient map preserving the set has the same fixed-point conclusion.

theorem ambient_fixedPoint_of_property
    (hX : HasNonexpansiveFixedPointProperty X)
    (C : Set X) (hC : C.Nonempty) (hclosed : IsClosed C)
    (hbounded : Bornology.IsBounded C) (hconvex : Convex ℝ C)
    (F : X → X) (hmap : Set.MapsTo F C C)
    (hF : ∀ a ∈ C, ∀ b ∈ C, ‖F a - F b‖ ≤ ‖a - b‖) :
    ∃ a ∈ C, F a = a := by
…

Mentions: OAI.ReflexiveFixedPoints.HasNonexpansiveFixedPointProperty