Model.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SeparableQuotient.CH line 12
Source documentation
The continuum hypothesis.
Also declared: ComparatorChallenges/SeparableQuotientNegative.lean:12 (same declaration text).
```
def CH : Prop := Cardinal.mk ℝ = Cardinal.aleph 1
```
def OAI.SeparableQuotient.HasSeparableQuotient line 15
Source documentation
A bounded linear surjection onto an infinite-dimensional separable Banach space.
Also declared: ComparatorChallenges/SeparableQuotientNegative.lean:15 (same declaration text).
```
def HasSeparableQuotient (𝕜 : Type) [RCLike 𝕜]
    (X : Type u) [NormedAddCommGroup X] [NormedSpace 𝕜 X] : Prop :=
…
```
def OAI.SeparableQuotient.SQ line 22
Source documentation
The separable quotient assertion at an arbitrary ambient universe.
Also declared: ComparatorChallenges/SeparableQuotientNegative.lean:22 (same declaration text).
```
def SQ (𝕜 : Type) [RCLike 𝕜] : Prop :=
…
```
def OAI.SeparableQuotient.RealValuedMeasurableContinuum line 29
Source documentation
The probability measure is defined on the full powerset of the continuum. The last clause quantifies over every smaller index set (represented as a subset of ℝ); ENNReal tsum is the supremum of finite subsums.
```
def RealValuedMeasurableContinuum : Prop :=
…
```