OAI/Combinatorics/BalancedRyser/Local/LocalParentMap.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.ParentMap.endpointIndex line 11
  2. theorem OAI.Balanced.Local.ParentMap.endpointIndex_injective line 14
  3. theorem OAI.Balanced.Local.ParentMap.endpointIndex_eq_or line 20
  4. def OAI.Balanced.Local.ParentMap.dependent line 27
  5. def OAI.Balanced.Local.ParentMap.underlying line 30
  6. theorem OAI.Balanced.Local.ParentMap.sub_one_ne line 35
  7. theorem OAI.Balanced.Local.ParentMap.underlying_first line 38
  8. theorem OAI.Balanced.Local.ParentMap.underlying_second line 42
  9. theorem OAI.Balanced.Local.ParentMap.underlying_fixed line 47
  10. theorem OAI.Balanced.Local.ParentMap.underlying_not_dependent line 53
  11. theorem OAI.Balanced.Local.ParentMap.underlying_idempotent line 64
  12. theorem OAI.Balanced.Local.ParentMap.underlying_injective_on_dependent line 71
  13. theorem OAI.Balanced.Local.ParentMap.two_anchors_not_both_self line 85
  14. theorem OAI.Balanced.Local.ParentMap.underlying_fiber_card_le_two line 101
  15. theorem OAI.Balanced.Local.ParentMap.endpoint_on_constituent line 132
  16. theorem OAI.Balanced.Local.ParentMap.endpoint_purposeful line 145
  17. theorem OAI.Balanced.Local.ParentMap.child_endpoint_eq_projection line 156
  18. theorem OAI.Balanced.Local.ParentMap.same_underlying_shared_constituent line 186
  19. theorem OAI.Balanced.Local.ParentMap.ordinary_anchor_not_self line 215
  20. theorem OAI.Balanced.Local.ParentMap.used_pair_anchor_not_self line 229