OAI/Analysis/CharacterCriterion/Reindexing.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KirchbergRordam.Reindex.diagonal_select line 29
2. lemma OAI.KirchbergRordam.NormUltrapower.quotient_eq_iff line 56
3. def OAI.KirchbergRordam.NormUltrapower.reindexed line 63
4. lemma OAI.KirchbergRordam.NormUltrapower.reindexed_apply line 66
5. inductive OAI.KirchbergRordam.NormUltrapower.ReindexTest line 69
6. theorem OAI.KirchbergRordam.NormUltrapower.countable_reindex line 76
7. def OAI.KirchbergRordam.RationalDense.stage line 182
8. lemma OAI.KirchbergRordam.RationalDense.stage_step line 186
9. lemma OAI.KirchbergRordam.RationalDense.stage_mono line 188
10. lemma OAI.KirchbergRordam.RationalDense.stage_countable line 189
11. def OAI.KirchbergRordam.RationalDense.termAlgebra line 194
12. lemma OAI.KirchbergRordam.RationalDense.term_countable line 216
13. lemma OAI.KirchbergRordam.RationalDense.subset_term line 218
14. theorem OAI.KirchbergRordam.RationalDense.exists_countable_dense_star line 221
15. theorem OAI.KirchbergRordam.RationalDense.extend_complex line 236
16. theorem OAI.KirchbergRordam.NormUltrapower.relative_commuting_copy line 277