OAI/ModelTheory/AbstractElementary/ModelExistence.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Models of prescribed cardinality in abstract elementary classes.

  1. structure OAI.EventualCategoricity.SetModel line 14
  2. instance OAI.EventualCategoricity.(instance at line 18) line 18
  3. def OAI.EventualCategoricity.SetModel.Submodel line 24
  4. def OAI.EventualCategoricity.SetModel.ImageOf line 27
  5. def OAI.EventualCategoricity.SetModel.card line 32
  6. structure OAI.EventualCategoricity.AEC line 36
  7. def OAI.EventualCategoricity.AEC.Categorical line 70
  8. def OAI.EventualCategoricity.AEC.UnboundedCategoricity line 75
  9. def OAI.EventualCategoricity.AEC.CategoricityTail line 78
  10. def OAI.EventualCategoricity.UniformEventualCategoricity line 83
  11. def OAI.EventualCategoricity.QualitativeEventualCategoricity line 88
  12. theorem OAI.EventualCategoricity.exists_subset_card line 92
  13. theorem OAI.EventualCategoricity.SetModel.Submodel.carrier_subset line 115
  14. theorem OAI.EventualCategoricity.SetModel.Submodel.card_le line 121
  15. theorem OAI.EventualCategoricity.SetModel.Submodel.of_carrier_subset line 124
  16. theorem OAI.EventualCategoricity.AEC.strong_of_carrier_subset line 152
  17. theorem OAI.EventualCategoricity.AEC.exists_small_strong_submodel line 157
  18. theorem OAI.EventualCategoricity.AEC.small_strong_submodels_directed line 165
  19. theorem OAI.EventualCategoricity.AEC.small_strong_submodels_cover line 184
  20. theorem OAI.EventualCategoricity.AEC.exists_strong_submodel_card_containing line 195
  21. theorem OAI.EventualCategoricity.AEC.exists_strong_submodel_card line 221
  22. theorem OAI.EventualCategoricity.AEC.arbitrarily_large_models line 228
  23. theorem OAI.EventualCategoricity.AEC.models_at_every_cardinal_above_LS line 233
  24. theorem OAI.EventualCategoricity.AEC.contains_copy_at_categorical_cardinal line 240