OAI/SetTheory/PartitionPrinciple/Geometry/GroundNiceRefinementVisibility.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.RefinementIndexLevelCode line 10
  2. theorem OAI.PartitionPilot.Forcing.RefinementIndexLevelCode.disjoint line 17
  3. theorem OAI.PartitionPilot.Forcing.RefinementIndexLevelCode.union_level_graph line 26
  4. theorem OAI.PartitionPilot.Forcing.RefinementIndexLevelCode.union_level_function line 65
  5. theorem OAI.PartitionPilot.Forcing.RefinementIndexLevelCode.union_level_entry line 77
  6. def OAI.PartitionPilot.Forcing.RefinementIndexSelectionCode line 94
  7. def OAI.PartitionPilot.Forcing.SetFormula.refinementIndexSelectionRawFormula line 105
  8. def OAI.PartitionPilot.Forcing.SetFormula.refinementIndexSelectionFormula line 117
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementIndexSelectionRawFormula line 127
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementIndexSelectionFormula line 148
  11. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndices line 186
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_refinementIndices line 191
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndexCode_mem_indices line 198
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndices_mem line 218
  15. def OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndices line 261
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndices_mem line 268
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndex_mem_iff line 283
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndices_fields line 336
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndices_field_function line 344
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndices_fields_ground line 351
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndices_level_graph line 371
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_niceRefinementIndex_fields line 395
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.normalizedRefinementIndex_mem line 421
  24. def OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexBounds line 475
  25. structure OAI.PartitionPilot.Forcing.NiceRefinementIndexSystem line 482
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexSystem line 514
  27. theorem OAI.PartitionPilot.Forcing.NiceRefinementIndexSystem.levelCode line 559
  28. theorem OAI.PartitionPilot.Forcing.NiceRefinementIndexSystem.different_levels_disjoint line 565
  29. theorem OAI.PartitionPilot.Forcing.NiceRefinementIndexSystem.union_level_data line 571
  30. structure OAI.PartitionPilot.Forcing.RefinementObjectSystem line 598
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementObjects line 626
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndex_preserves_visibility line 699