OAI/ModelTheory/Categoricity/Collapse.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CHObstruction.TaggedCollapse.collapse line 17
  2. theorem OAI.CHObstruction.TaggedCollapse.collapse_eq line 20
  3. theorem OAI.CHObstruction.TaggedCollapse.mem_collapse line 24
  4. theorem OAI.CHObstruction.TaggedCollapse.injective line 29
  5. theorem OAI.CHObstruction.TaggedCollapse.rank_le line 54
  6. def OAI.CHObstruction.TaggedCollapse.embedding line 64
  7. theorem OAI.CHObstruction.TaggedCollapse.wellFounded_of_tags line 72
  8. abbrev OAI.CHObstruction.Domination.Alpha line 80
  9. abbrev OAI.CHObstruction.Domination.Beta line 81
  10. def OAI.CHObstruction.Domination.indexEmbedding line 83
  11. theorem OAI.CHObstruction.Domination.countable_Iio line 95
  12. def OAI.CHObstruction.Domination.Prior line 100
  13. instance OAI.CHObstruction.Domination.prior_countable line 103
  14. def OAI.CHObstruction.Domination.values line 113
  15. theorem OAI.CHObstruction.Domination.values_eq line 122
  16. theorem OAI.CHObstruction.Domination.eventually_lt line 128
  17. theorem OAI.CHObstruction.Domination.countable_exceptions line 134
  18. def OAI.CHObstruction.CountableClosures.witness line 158
  19. theorem OAI.CHObstruction.CountableClosures.witness_distinguishes line 162
  20. def OAI.CHObstruction.CountableClosures.stage line 166
  21. def OAI.CHObstruction.CountableClosures.closure line 170
  22. theorem OAI.CHObstruction.CountableClosures.stage_mono line 172
  23. theorem OAI.CHObstruction.CountableClosures.subset_closure line 177
  24. theorem OAI.CHObstruction.CountableClosures.closure_mono line 180
  25. theorem OAI.CHObstruction.CountableClosures.closure_countable line 195
  26. theorem OAI.CHObstruction.CountableClosures.witness_mem line 203
  27. theorem OAI.CHObstruction.CountableClosures.extensional line 212
  28. abbrev OAI.CHObstruction.CountableClosures.FiniteSeed line 218
  29. def OAI.CHObstruction.CountableClosures.entries line 220
  30. theorem OAI.CHObstruction.CountableClosures.entries_countable line 222
  31. theorem OAI.CHObstruction.CountableClosures.seed_subset line 225
  32. theorem OAI.CHObstruction.CountableClosures.entries_nonempty line 228
  33. theorem OAI.CHObstruction.CountableClosures.entries_mono line 231
  34. def OAI.CHObstruction.CountableClosures.enumeration line 235
  35. theorem OAI.CHObstruction.CountableClosures.enumeration_surjective line 243
  36. theorem OAI.CHObstruction.CountableClosures.enumeration_singleton line 251
  37. theorem OAI.CHObstruction.CountableClosures.membership_separates line 255
  38. def OAI.CHObstruction.TaggedLimit.relation line 281
  39. def OAI.CHObstruction.TaggedLimit.rankTag line 284
  40. theorem OAI.CHObstruction.TaggedLimit.relation_mk line 287
  41. theorem OAI.CHObstruction.TaggedLimit.rankTag_mk line 291
  42. theorem OAI.CHObstruction.TaggedLimit.extensional line 294
  43. theorem OAI.CHObstruction.TaggedLimit.decreases line 305
  44. def OAI.CHObstruction.TaggedLimit.embedding line 312