OAI/SetTheory/PartitionPrinciple/Models/IncidenceQuotient.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.realizes_of_equation line 13
  2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.parents_of_equations line 20
  3. inductive OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.EdgeRelated line 28
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.edgeSetoid line 38
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.EdgeQuotient line 41
  6. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.edgeClass line 42
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.edge_class_equation line 45
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.parent_related_edge line 48
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.edge_related_sound line 57
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.exact_edge_identifications line 65
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.edge_related_iff_parent line 72