OAI/Combinatorics/BalancedRyser/Local/GlobalAlignedParentCoordinates.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.Local.AlignedGlobal.freeCoordinates line 16
  2. def OAI.Balanced.Local.AlignedGlobal.underlyingFree line 21
  3. theorem OAI.Balanced.Local.AlignedGlobal.free_point_eq_coordinate line 30
  4. theorem OAI.Balanced.Local.AlignedGlobal.point_eq_of_underlying_coordinate_eq line 40
  5. theorem OAI.Balanced.Local.AlignedGlobal.point_eq_of_free_coordinate_eq line 80
  6. def OAI.Balanced.Local.AlignedGlobal.pointFromCoordinate line 89
  7. theorem OAI.Balanced.Local.AlignedGlobal.point_eq_parent_projection line 100
  8. theorem OAI.Balanced.Local.AlignedGlobal.point_eq_pointFromCoordinate line 129
  9. theorem OAI.Balanced.Local.AlignedGlobal.pointFromCoordinate_free line 147
  10. structure OAI.Balanced.Local.AlignedGlobal.PointSystem line 168
  11. def OAI.Balanced.Local.AlignedGlobal.pointSystemOfNoDependents line 179
  12. def OAI.Balanced.Local.AlignedGlobal.pointSystemOfLinkedPair line 192
  13. theorem OAI.Balanced.Local.AlignedGlobal.exists_smallReuse_pointSystem line 211