OAI/Analysis/CircleDomains/Selection/FiniteLineGaps.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual gaps of finitely many disjoint line intervals

Sorting the closed holes supplies the open intervals on which variation is paid. Every gap is nonempty, the gaps are disjoint, and no point of a gap belongs to a hole. Point holes are allowed.

  1. def OAI.CircleDomainRigidity.gapsAfterHoles line 21
  2. theorem OAI.CircleDomainRigidity.gapsAfterHoles_zero_fst line 25
  3. theorem OAI.CircleDomainRigidity.gapsAfterHoles_last_snd line 28
  4. theorem OAI.CircleDomainRigidity.gapsAfterHoles_succ_fst line 31
  5. theorem OAI.CircleDomainRigidity.gapsAfterHoles_castSucc_snd line 35
  6. theorem OAI.CircleDomainRigidity.gapsAfterHoles_strict line 39
  7. theorem OAI.CircleDomainRigidity.gapsAfterHoles_avoid line 55
  8. theorem OAI.CircleDomainRigidity.gapsAfterHoles_disjoint line 74
  9. theorem OAI.CircleDomainRigidity.interval_right_lt_left_of_disjoint line 98
  10. theorem OAI.CircleDomainRigidity.sorted_holes_separated line 105