SourceTargetEnds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A target component corresponding to a source component

For the same sequence of matched boundary labels, the nested source disks intersect in the original complementary component and the nested target disks intersect in a full target complementary component.

theorem OAI.CircleDomainRigidity.corresponding_target_end_of_source_of_continuous_open line 22
theorem OAI.CircleDomainRigidity.corresponding_target_end_of_source line 97

theorem OAI.CircleDomainRigidity.corresponding_source_end_of_target_of_continuous_open line 122

Source documentation

Conversely every target complementary component has a source component with the same matched boundary address.

theorem corresponding_source_end_of_target_of_continuous_open
    {G : Set Sphere} (hG : IsOpen G) {f : Sphere → Sphere}
    (hf : ContinuousOn f G)
    (ho : ∀ S, IsOpen S → S ⊆ G → IsOpen (f '' S)) (hi : InjOn f G)
    (C : ℕ → SmoothJordanCore G) (J : (n : ℕ) → Fin (C n).count → ℂ ≃ₜ ℂ)
    (hstrict : ∀ n, (C n).carrier ⊆ interior (C (n + 1)).carrier)
    (hcover : (⋃ n, interior (C n).carrier) = G)
    (hJd : ∀ n, Pairwise (Disjoint on fun i => closure (jordanInterior (J n i))))
    (hJe : ∀ n, (f '' (C n).carrier)ᶜ = ⋃ i, ((↑) : ℂ → Sphere) '' jordanInterior (J n i))
    (hboundary : ∀ n i, f '' (((↑) : ℂ → Sphere) '' frontier (jordanInterior ((C n).disk i))) =
      ((↑) : ℂ → Sphere) '' frontier (jordanInterior (J n i)))
    (hside : ∀ n i, f '' (G ∩ (((↑) : ℂ → Sphere) '' jordanInterior ((C n).disk i))) =
…

Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.SmoothJordanCore, OAI.CircleDomainRigidity.jordanInterior

theorem OAI.CircleDomainRigidity.corresponding_source_end_of_target line 192

theorem OAI.CircleDomainRigidity.exists_matched_component_exhaustion_of_continuous_open line 218

Source documentation

The constructed smooth exhaustion gives every complementary component on either side a matched source/target address. Only the previously used Sard, one-manifold classification and Schoenflies inputs enter the construction.

theorem exists_matched_component_exhaustion_of_continuous_open
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {G : Set Sphere} (hG : IsOpen G) (hconn : IsConnected G)
    (hinf : OnePoint.infty ∈ G)
    {f : Sphere → Sphere} (hf : ContinuousOn f G)
    (ho : ∀ S, IsOpen S → S ⊆ G → IsOpen (f '' S)) (hi : InjOn f G)
    (hfix : f OnePoint.infty = OnePoint.infty) :
    ∃ (C : ℕ → SmoothJordanCore G) (J : (n : ℕ) → Fin (C n).count → ℂ ≃ₜ ℂ),
      (∀ n, (C n).carrier ⊆ interior (C (n + 1)).carrier) ∧
      (⋃ n, interior (C n).carrier) = G ∧
      (∀ q ∈ Gᶜ, ∃ (b : (n : ℕ) → Fin (C n).count) (p : Sphere),
        p ∈ (f '' G)ᶜ ∧
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.SmoothJordanCore

theorem OAI.CircleDomainRigidity.exists_matched_component_exhaustion line 248