OAI/Analysis/CircleDomains/Selection/AnalyticWordBranch.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A branch through finite Baire words identifies an actual point of a continuous image. This is the topological step for completed measurability.

  1. def OAI.CircleDomainRigidity.baireWordCylinder line 13
  2. theorem OAI.CircleDomainRigidity.baireWordCylinder_nil line 16
  3. theorem OAI.CircleDomainRigidity.baireWordCylinder_children line 20
  4. theorem OAI.CircleDomainRigidity.isOpen_baireWordCylinder line 30
  5. theorem OAI.CircleDomainRigidity.eq_of_prefix_closures line 42
  6. theorem OAI.CircleDomainRigidity.mem_range_of_prefix_closures line 58
  7. theorem OAI.CircleDomainRigidity.mem_range_of_word_hull_branch line 63