OAI/SetTheory/PartitionPrinciple/Models/CopyQuotient.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.Node line 13
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.point line 15
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.nodeLe line 17
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.mk_le_mk line 22
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.mk_eq_mk line 25
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.node_refl line 28
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.node_trans line 32
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.node_antisymm line 36
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.vertex_le line 40
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.vertex_below line 43
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.cover line 47
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.vertex_ideal line 51
  13. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.IsMeet line 58
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.cross_meet_spec line 61
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.all_meets line 70
  16. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.order line 74
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.meet_eq line 84
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.vertex_meet_spec line 88
  19. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.vertex line 97
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.vertex_injective line 102
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.exact_overlap line 105
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.cross_meet line 110
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.part_respects line 115
  24. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.projection line 123
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.greatest_part line 126
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.projection_formula line 131
  27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.vertex_principal line 134
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.bottom_preserved line 141
  29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.comparison_in_vertex line 145