`OAI/Analysis/SeparableQuotients/NegativeReal.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SeparableQuotient.negative_real line 13
Source documentation
CH refutes the real separable quotient assertion in every universe.
```
theorem negative_real (hCH : CH) : ¬ SQ.{u} ℝ := by
…
```
Mentions: OAI.SeparableQuotient.CH