OAI/Analysis/CircleDomains/Topology/DyadicOpenCover.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A countable cover of an open time set by closed dyadic intervals inside it.

  1. theorem OAI.CircleDomainRigidity.exists_dyadicCell_mem line 14
  2. abbrev OAI.CircleDomainRigidity.DyadicInside line 30
  3. def OAI.CircleDomainRigidity.insideDyadicCell line 33
  4. theorem OAI.CircleDomainRigidity.iUnion_insideDyadicCell line 36