OAI/Analysis/CircleDomains/Topology/HomeomorphicLevelContinuum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Initial pieces of actual horizontal inverse lines provide compact level continua from the centre to the boundary of any closed disk.

  1. theorem OAI.CircleDomainRigidity.homeomorphic_level_continuum line 13