OAI/Analysis/CircleDomains/Topology/JordanDiskImages.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CircleDomainRigidity.planar_interior_image line 15
2. theorem OAI.CircleDomainRigidity.planar_frontier_image line 32
3. theorem OAI.CircleDomainRigidity.open_eq_jordan_of_frontier line 42
4. theorem OAI.CircleDomainRigidity.open_eq_jordanInterior_of_frontier line 65

   Source documentation

   An open bounded region with the boundary of a Jordan disk is that disk.

   theorem open_eq_jordanInterior_of_frontier
       (H : ℂ ≃ₜ ℂ) {U : Set ℂ} (hU : IsOpen U) (hb : Bornology.IsBounded U)
       (hne : U.Nonempty) (hf : frontier U = frontier (jordanInterior H)) :
       U = jordanInterior H := open_eq_jordan_of_frontier H hU hb hne hf

   Mentions: OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.open_eq_jordan_of_frontier

5. theorem OAI.CircleDomainRigidity.exists_jordan_image_disk line 72

   Source documentation

   The images are the whole Jordan interior and its closure, rather than merely subsets of the corresponding sides, by planar Schoenflies.

   theorem exists_jordan_image_disk (hsch : PlanarSchoenflies)
       {f : ℂ → ℂ} {G : Set ℂ} (hG : IsOpen G) (hc : ContinuousOn f G)
       (ho : ∀ S, IsOpen S → S ⊆ G → IsOpen (f '' S)) (hi : InjOn f G)
       (H : ℂ ≃ₜ ℂ) (hHG : closure (jordanInterior H) ⊆ G) :
       ∃ K : ℂ ≃ₜ ℂ,
         f '' jordanInterior H = jordanInterior K ∧
         f '' closure (jordanInterior H) = closure (jordanInterior K) ∧
         frontier (jordanInterior K) = f '' frontier (jordanInterior H) := by
   …

   Mentions: OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.jordanInterior