OAI/Analysis/JiangSu/CentralSequences/CountableArraySaturation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NormUltra.bounded_countable_array_test line 18
  2. lemma OAI.NonunitalCentralSaturation.exists_bounded_lift line 60
  3. lemma OAI.NonunitalCentralSaturation.central_representative_errors line 70
  4. lemma OAI.NonunitalCentralSaturation.quotient_eq_of_dense_errors line 77
  5. abbrev OAI.NonunitalCentralSaturation.Var line 122
  6. instance OAI.NonunitalCentralSaturation.(instance at line 123) line 123
  7. inductive OAI.NonunitalCentralSaturation.Test line 124
  8. instance OAI.NonunitalCentralSaturation.(instance at line 132) line 132
  9. def OAI.NonunitalCentralSaturation.baseBound line 134
  10. lemma OAI.NonunitalCentralSaturation.baseBound_nonneg line 137
  11. def OAI.NonunitalCentralSaturation.FiniteModels line 139
  12. def OAI.NonunitalCentralSaturation.testValue line 143
  13. lemma OAI.NonunitalCentralSaturation.testValue_nonneg line 151
  14. def OAI.NonunitalCentralSaturation.Test.terms line 157
  15. theorem OAI.NonunitalCentralSaturation.finite_models_coordinate_supply line 163