OAI/Analysis/CircleDomains/Topology/RealInjectiveOpenImage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The one-dimensional open-image fact needed to recognize a Jordan boundary inside a regular scalar level. Only interval monotonicity and the intermediate value theorem are used.

  1. lemma OAI.CircleDomainRigidity.real_injective_interval_image_mem_nhds line 14
  2. lemma OAI.CircleDomainRigidity.real_open_image_of_continuousOn_injOn line 31