OAI/Analysis/Kaplansky/Ultrapower/PolarScalar.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyConsequences.PolarScalar.invCut line 11
2. def OAI.KaplanskyConsequences.PolarScalar.cut line 12
3. lemma OAI.KaplanskyConsequences.PolarScalar.max_pos line 14
4. lemma OAI.KaplanskyConsequences.PolarScalar.continuous_invCut line 15
5. lemma OAI.KaplanskyConsequences.PolarScalar.continuous_cut line 17
6. lemma OAI.KaplanskyConsequences.PolarScalar.invCut_nonneg line 20
7. lemma OAI.KaplanskyConsequences.PolarScalar.cut_nonneg line 21
8. lemma OAI.KaplanskyConsequences.PolarScalar.cut_le_one line 22
9. lemma OAI.KaplanskyConsequences.PolarScalar.cut_eq line 25
10. lemma OAI.KaplanskyConsequences.PolarScalar.cut_mono line 34
11. lemma OAI.KaplanskyConsequences.PolarScalar.cut_gap line 39
12. lemma OAI.KaplanskyConsequences.PolarScalar.cut_error line 59