Model.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ReflexiveFixedPoints.CanonicallyReflexive line 14
Source documentation
Surjectivity of the canonical map into the continuous bidual.
Also declared: ComparatorChallenges/ReflexiveFixedPoints.lean:14 (same declaration text).
```
def CanonicallyReflexive : Prop :=
…
```
def OAI.ReflexiveFixedPoints.NonexpansiveOn line 20
Source documentation
Nonexpansiveness is measured in the original ambient norm.
```
def NonexpansiveOn (C : Set X) (F : C → C) : Prop :=
…
```
def OAI.ReflexiveFixedPoints.HasNonexpansiveFixedPointProperty line 25
Source documentation
Every nonexpansive selfmap of every nonempty closed bounded convex set has a fixed point, in the norm already carried by X.
```
def HasNonexpansiveFixedPointProperty (X : Type u)
    [NormedAddCommGroup X] [NormedSpace ℝ X] : Prop :=
…
```