OAI/Analysis/JiangSu/CentralSequences/NormUltrapowerArrayTest.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NormUltra.bounded_array_test line 17
2. theorem OAI.NormUltra.bounded_array_test_countable line 47
3. def OAI.NormUltra.CentralFiniteModels line 80
4. abbrev OAI.NormUltra.Test line 85
5. instance OAI.NormUltra.(instance at line 86) line 86
6. def OAI.NormUltra.testValue line 87
7. lemma OAI.NormUltra.testValue_nonneg line 91
8. theorem OAI.NormUltra.central_rational_saturation line 97