OAI/SetTheory/PartitionPrinciple/Models/GroundRefinementQuotientNames.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.refinementQuotientMap line 12
  2. theorem OAI.PartitionPilot.Forcing.refinementQuotientMap_subset line 17
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_refinementQuotientMap line 24
  4. theorem OAI.PartitionPilot.Forcing.mem_refinementQuotientMap line 41
  5. theorem OAI.PartitionPilot.Forcing.refinementQuotientMap_class_entry line 52
  6. theorem OAI.PartitionPilot.Forcing.equivalenceClass_refinement_subset line 57
  7. theorem OAI.PartitionPilot.Forcing.refinementQuotientMap_value_iff line 63
  8. theorem OAI.PartitionPilot.Forcing.refinementQuotientMap_function line 77
  9. theorem OAI.PartitionPilot.Forcing.refinementQuotientMap_onto line 88
  10. theorem OAI.PartitionPilot.Forcing.refinementQuotientMap_entry_iff_subset line 95
  11. theorem OAI.PartitionPilot.Forcing.refinementQuotientMap_member_value line 112
  12. theorem OAI.PartitionPilot.Forcing.refinementQuotientMap_triangle line 122
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementQuotientMap_mem line 160
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementQuotientMap_spec line 174
  15. theorem OAI.PartitionPilot.Forcing.equivalenceClass_eq_of_carrier_subset line 201
  16. def OAI.PartitionPilot.Forcing.Name.refinementQuotient line 213
  17. def OAI.PartitionPilot.Forcing.Name.refinementNaturalMap line 217
  18. theorem OAI.PartitionPilot.Forcing.Name.entry_refinementQuotient line 222
  19. theorem OAI.PartitionPilot.Forcing.Name.entry_refinementNaturalMap line 228
  20. theorem OAI.PartitionPilot.Forcing.Name.eval_refinementQuotient line 235
  21. theorem OAI.PartitionPilot.Forcing.Name.eval_refinementNaturalMap line 260
  22. theorem OAI.PartitionPilot.Forcing.Name.act_refinementQuotient line 307
  23. theorem OAI.PartitionPilot.Forcing.Name.act_refinementNaturalMap line 314
  24. theorem OAI.PartitionPilot.Forcing.Name.refinementQuotient_support line 325
  25. theorem OAI.PartitionPilot.Forcing.Name.refinementNaturalMap_support line 332
  26. theorem OAI.PartitionPilot.Forcing.Name.refinementClass_hs_of_hs line 340
  27. theorem OAI.PartitionPilot.Forcing.Name.refinementQuotient_hs line 349
  28. theorem OAI.PartitionPilot.Forcing.Name.refinementNaturalMap_hs line 362
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementQuotient_mem line 395
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementNaturalMap_mem line 406