OAI/SetTheory/PartitionPrinciple/Transfinite/ChronologicalTheorem.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.CountableBelow line 13
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.CountableBasis line 17
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.AllFiltersCountable line 19
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.countableBelow_mono line 21
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.countableBelow_empty line 26
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.countableBelow_of_countable line 30
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.countableBelow_union line 35
  8. def OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.pullFilter line 50
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.countableBelow_copy line 59
  10. def OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.Essential line 79
  11. def OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.EssentialStages line 82
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.positive_above_essential line 85
  13. def OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.OldMeet line 95
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.essential_below_earlier line 98
  15. def OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.DescendingCountable line 111
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.essential_stages_countable line 115
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.countable_basis_of_layers line 132
  18. def OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.OldBridge line 161
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.essentials_no_bridge line 166
  20. inductive OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.GrowthLayer line 177
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.GrowthLayer.countable_essentials line 191
  22. structure OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.History line 224
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.History.all_filters_countable line 233