OAI/Analysis/CircleDomains/Selection/TerminalRemainder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The safe region for filling after the terminals are selected

The remaining quotient dust is compact and relatively clopen. Its open neighborhood is chosen to avoid both the retained physical core and all closed terminal caps, so every later filling closure inherits both separations.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.terminalRemainder line 22
  2. def OAI.CircleDomainRigidity.FiniteTransfer.closedTerminalImages line 25
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.terminal_remainder_safe_region line 28
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.PhysicalTerminalDisks.index_mem_quotient_union line 56
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.PhysicalTerminalDisks.remainder_avoids_indices line 67
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.filling_closures_avoid_core_and_terminals line 78

    Source documentation

    Every closed filling drawn in the safe region misses both the core and every closed terminal cap.

    theorem filling_closures_avoid_core_and_terminals
    {I J : Type*} {C : Set Sphere} {π : Sphere → Sphere}
    (T : I → ℂ ≃ₜ ℂ) (F : J → ℂ ≃ₜ ℂ)
    (hF : ∀ j, closure (jordanInterior (F j)) ⊆
      (fun z : ℂ => π (z : Sphere)) ⁻¹' ((π '' C)ᶜ ∩ (closedTerminalImages π T)ᶜ)) :
    (∀ j, Disjoint (((↑) : ℂ → Sphere) '' closure (jordanInterior (F j))) C) ∧
      ∀ i j, Disjoint (closure (jordanInterior (T i))) (closure (jordanInterior (F j))) := by
…

    Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.closedTerminalImages