ExteriorSeparation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Trapping the bounded side of a circle-model image

A compact exterior piece has closed image. Its open interior has open image, and their difference is the image of the boundary circle. A connected set avoiding that boundary and meeting the open image must lie entirely in the image. This supplies the topological part of the uniform bound for finite circle models.

theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.isOpen_image line 23
theorem OAI.CircleDomainRigidity.connected_set_subset_image_of_boundary_avoidance line 39

theorem OAI.CircleDomainRigidity.sphere_exterior_subset_image line 63

Source documentation

A geometric boundary inclusion traps every exterior target point in an exterior source image. The coefficient bound will supply the inclusion.

theorem sphere_exterior_subset_image
    {f fi : Sphere → Sphere} {U V : Set Sphere} (hf : IsSmoothSphereEquivalence f fi U V)
    (hV : IsOpen V) {r L : ℝ} (_hr : 0 < r) (hL : 0 ≤ L)
    (hEU : ((((↑) : ℂ → Sphere) '' Metric.ball 0 r)ᶜ) ⊆ U)
    (hfix : f OnePoint.infty = OnePoint.infty)
    (hboundary : ∀ z : ℂ, ‖z‖ = r → f (z : Sphere) ∈
      ((↑) : ℂ → Sphere) '' Metric.closedBall 0 L) :
    ((((↑) : ℂ → Sphere) '' Metric.closedBall 0 L)ᶜ) ⊆
      f '' ((((↑) : ℂ → Sphere) '' Metric.closedBall 0 r)ᶜ) := by
…

Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsSmoothSphereEquivalence