OAI/Analysis/Kaplansky/Ultrapower/Construction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyConsequences.QuasiValue.ultra_tendsto line 15
2. abbrev OAI.KaplanskyConsequences.QuasiValue.Sequences line 26
3. lemma OAI.KaplanskyConsequences.QuasiValue.seq_eval_selfAdjoint line 29
4. lemma OAI.KaplanskyConsequences.QuasiValue.seq_eval_commute line 33
5. lemma OAI.KaplanskyConsequences.QuasiValue.ultra_val_tendsto line 37
6. def OAI.KaplanskyConsequences.QuasiValue.ultra line 41
7. def OAI.KaplanskyConsequences.QuasiValue.constHom line 97
8. lemma OAI.KaplanskyConsequences.QuasiValue.constHom_apply line 106
9. lemma OAI.KaplanskyConsequences.QuasiValue.ultra_const line 108