OAI/Analysis/CharacterCriterion/CentralSequences.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.NormUltrapower.exists_bounded_representative line 34
2. inductive OAI.KirchbergRordam.NormUltrapower.CollapseTest line 43
3. def OAI.KirchbergRordam.NormUltrapower.CollapseTest.eval line 51
4. lemma OAI.KirchbergRordam.NormUltrapower.CollapseTest.natural line 60
5. lemma OAI.KirchbergRordam.NormUltrapower.CollapseTest.apply_seq line 66
6. theorem OAI.KirchbergRordam.NormUltrapower.countable_iterated_collapse line 73
7. theorem OAI.KirchbergRordam.NormUltrapower.iterated_central_collapse line 193