OAI/Analysis/CircleDomains/Topology/HomeomorphicCoordinateRange.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A coordinate of a plane homeomorphism has no interior extremum. Its bounds on the boundary of any compact set hold throughout that set.

  1. theorem OAI.CircleDomainRigidity.homeomorphic_im_not_local_max line 15
  2. theorem OAI.CircleDomainRigidity.homeomorphic_im_not_local_min line 23
  3. theorem OAI.CircleDomainRigidity.homeomorphic_im_le_of_boundary line 31
  4. theorem OAI.CircleDomainRigidity.homeomorphic_im_ge_of_boundary line 42