ChartTopology.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Openness of the limiting coordinate chart

Euclidean invariance of domain is formulated as an open-image property, following Hatcher, Algebraic Topology (2002), Theorem 2B.3, page 172. The metric estimates use the ambient subtype distance.

def OAI.RegularPointCoordinates.EuclideanInvarianceOfDomain line 19
Source documentation
Precisely the Euclidean open-image assertion of Hatcher, Theorem 2B.3.
```
def EuclideanInvarianceOfDomain (n : ℕ) : Prop :=
…
```

theorem OAI.RegularPointCoordinates.isOpen_range_of_coordinates line 24

Source documentation

Transfer invariance of domain through the original topological coordinates.

theorem isOpen_range_of_coordinates {X : Type*} [TopologicalSpace X] {n : ℕ}
    (hIOD : EuclideanInvarianceOfDomain n) {O : Set (Euclidean n)} (hO : IsOpen O)
    (u : X ≃ₜ O) {F : X → Euclidean n} (hF : Continuous F)
    (hinj : Function.Injective F) : IsOpen (range F) := by
…

Mentions: OAI.RegularPointCoordinates.EuclideanInvarianceOfDomain, OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.hasOpenBilipschitzChart_of_coordinates_and_bounds line 41

Source documentation

Two-sided ambient-distance bounds and topological coordinates give an open bi-Lipschitz chart.

theorem hasOpenBilipschitzChart_of_coordinates_and_bounds
    {X : Type*} [MetricSpace X] {n : ℕ} {p : X}
    (hIOD : EuclideanInvarianceOfDomain n)
    {U : Set X} (hU : IsOpen U) (hp : p ∈ U)
    {O : Set (Euclidean n)} (hO : IsOpen O) (u : U ≃ₜ O)
    {F : U → Euclidean n} {L : ℝ} (hL : 1 ≤ L)
    (hbound : ∀ x z : U,
      L⁻¹ * dist (x : X) (z : X) ≤ dist (F x) (F z) ∧
      dist (F x) (F z) ≤ L * dist (x : X) (z : X)) :
    HasOpenBilipschitzChart n p := by
…

Mentions: OAI.RegularPointCoordinates.EuclideanInvarianceOfDomain, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.HasOpenBilipschitzChart