OAI/Analysis/CircleDomains/Topology/TerminalArcSet.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The endpoint and interior conditions of the compact arc reduction form a Borel set. Consequently a full law of these arcs has a compact core.

  1. lemma OAI.CircleDomainRigidity.measurableSet_pathsInsideOpenTime line 22
  2. def OAI.CircleDomainRigidity.terminalArcSet line 39
  3. lemma OAI.CircleDomainRigidity.measurableSet_terminalArcSet line 43
  4. theorem OAI.CircleDomainRigidity.terminalArcLaw_mem line 50
  5. theorem OAI.CircleDomainRigidity.exists_compact_terminal_arc_core line 67