OAI/Combinatorics/TriangleRemoval/Process/Parent.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.TriangleGrowth.Parent line 20
  2. def OAI.SharpTerminalLeave.TriangleGrowth.Ancestor line 22
  3. lemma OAI.SharpTerminalLeave.TriangleGrowth.parent_older line 24
  4. lemma OAI.SharpTerminalLeave.TriangleGrowth.parent_le line 27
  5. lemma OAI.SharpTerminalLeave.TriangleGrowth.ancestor_le line 30
  6. lemma OAI.SharpTerminalLeave.TriangleGrowth.ancestor_trans line 35
  7. lemma OAI.SharpTerminalLeave.TriangleGrowth.older_ancestor line 38
  8. def OAI.SharpTerminalLeave.TriangleGrowth.pathUnion line 56
  9. lemma OAI.SharpTerminalLeave.TriangleGrowth.mem_pathUnion line 60
  10. lemma OAI.SharpTerminalLeave.TriangleGrowth.left_mem_pathUnion line 65
  11. lemma OAI.SharpTerminalLeave.TriangleGrowth.right_mem_pathUnion line 68
  12. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathUnion_older_closed line 71
  13. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathUnion_subset_lower line 81