OAI/Analysis/Kaplansky/Ultrapower/UltraSaturation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.KaplanskyConsequences.QuasiValue.StarTerm line 15
2. def OAI.KaplanskyConsequences.QuasiValue.StarTerm.eval line 24
3. lemma OAI.KaplanskyConsequences.QuasiValue.StarTerm.map_eval line 31
4. instance OAI.KaplanskyConsequences.QuasiValue.seq_nontrivial line 39
5. abbrev OAI.KaplanskyConsequences.QuasiValue.UltraQuotient line 42
6. abbrev OAI.KaplanskyConsequences.QuasiValue.ultraHom line 43
7. abbrev OAI.KaplanskyConsequences.QuasiValue.ultraQ line 44
8. def OAI.KaplanskyConsequences.QuasiValue.seqEvalHom line 46
9. lemma OAI.KaplanskyConsequences.QuasiValue.ultra_q_tendsto line 55
10. lemma OAI.KaplanskyConsequences.QuasiValue.ultra_realize line 61