ConnectedCollars.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Connected compact neighborhoods of filling boundaries

Small closed metric thickenings of a compact connected planar curve are connected and compact. They give connected collars inside any prescribed open boundary neighborhood, as required for simultaneous staircase inactivity. No smooth tubular-neighborhood theorem is needed.

theorem OAI.CircleDomainRigidity.FiniteTransfer.isConnected_cthickening line 21
theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_compact_connected_neighborhood line 46
theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_compact_connected_jordan_collar line 58
Source documentation
A connected compact collar may be kept inside the domain, inside the relevant mask, and away from every inactive grid by choosing U to be the intersection of those open boundary neighborhoods.
```
theorem exists_compact_connected_jordan_collar
    (H : ℂ ≃ₜ ℂ) {U : Set ℂ} (hU : IsOpen U)
    (hboundary : frontier (jordanInterior H) ⊆ U) :
    ∃ K : Set ℂ, IsCompact K ∧ IsConnected K ∧
      K ∈ 𝓝ˢ (frontier (jordanInterior H)) ∧ K ⊆ U := by
…
```
Mentions: OAI.CircleDomainRigidity.jordanInterior