OAI/SetTheory/PartitionPrinciple/Geometry/CompressionUnionBaseFilling.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.mapFamilySection_union line 9
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundMapUnionFamily line 42
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundMeetEmbeddingUnionFamily line 76
  4. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_groundUnionMaps line 143
  5. structure OAI.PartitionPilot.Forcing.GroundCompressionAlgebra line 178
  6. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_groundAlgebra line 200
  7. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_fresh_accounting line 237
  8. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_map_equivariant line 286
  9. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_map_agrees_on_source line 309
  10. theorem OAI.PartitionPilot.Forcing.GroundCompressionAlgebra.map_eq_section line 344
  11. theorem OAI.PartitionPilot.Forcing.GroundCompressionAlgebra.maps_eq_sections line 366
  12. def OAI.PartitionPilot.Forcing.GroundCompressionAlgebra.bases line 399
  13. def OAI.PartitionPilot.Forcing.GroundCompressionAlgebra.caps line 403
  14. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_sources_function line 417
  15. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_top_arguments_function line 423
  16. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_bases_function line 432
  17. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_caps_function line 436
  18. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_base_entry_iff line 440
  19. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_cap_entry_iff line 448
  20. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_markings_ground line 457
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialCompressionAlgebra line 481
  22. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_top line 533
  23. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_map_base_filling line 546
  24. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_map_range_below_cap line 561