OAI/SetTheory/PartitionPrinciple/Definability/InitialMainAlgebraCodes.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.InitialMainAlgebra.carrier line 10
  2. def OAI.PartitionPilot.Forcing.InitialMainAlgebra.actors line 11
  3. def OAI.PartitionPilot.Forcing.InitialMainAlgebra.bottom line 12
  4. def OAI.PartitionPilot.Forcing.InitialMainAlgebra.top line 13
  5. def OAI.PartitionPilot.Forcing.InitialMainAlgebra.identity line 14
  6. def OAI.PartitionPilot.Forcing.InitialMainAlgebra.order line 15
  7. def OAI.PartitionPilot.Forcing.InitialMainAlgebra.meetGraph line 17
  8. def OAI.PartitionPilot.Forcing.InitialMainAlgebra.multiplication line 22
  9. def OAI.PartitionPilot.Forcing.InitialMainAlgebra.inverse line 23
  10. def OAI.PartitionPilot.Forcing.InitialMainAlgebra.action line 24
  11. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.bottom_ne_top line 27
  12. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.mem_carrier line 32
  13. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.mem_actors line 37
  14. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.bottom_mem line 42
  15. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.top_mem line 43
  16. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.identity_mem line 44
  17. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.pair_mem_order line 46
  18. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.pair_mem_meetGraph line 50
  19. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.pair_mem_multiplication line 56
  20. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.pair_mem_inverse line 60
  21. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.pair_mem_action line 63
  22. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.least line 67
  23. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.greatest line 70
  24. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.meet_function line 73
  25. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.meet_code line 88
  26. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.group_code line 126
  27. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.action_code line 171