Documentation

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Extended charts in smooth manifolds #

In a C^n manifold with corners with the model I on (E, H), the charts take values in the model space H. However, we also need to use extended charts taking values in the model vector space E. These extended charts are not PartialHomeomorph as the target is not open in E in general, but we can still register them as PartialEquiv.

Main definitions #

PartialHomeomorph.extend: compose a partial homeomorphism into H with the model I, to obtain a PartialEquiv into E. Extended charts are an example of this.
extChartAt I x: the extended chart at x, obtained by composing the chartAt H x with I. Since the target is in general not open, this is not a partial homeomorphism in general, but we register them as PartialEquivs.

Main results #

contDiffOn_extend_coord_change: if f and f' lie in the maximal atlas on M, f.extend I ∘ (f'.extend I).symm is continuous on its source
contDiffOn_ext_coord_change: for x x : M, the coordinate change (extChartAt I x').symm ≫ extChartAt I x is continuous on its source
Manifold.locallyCompact_of_finiteDimensional: a finite-dimensional manifold modelled on a locally compact field (such as ℝ, ℂ or the p-adic numbers) is locally compact
LocallyCompactSpace.of_locallyCompact_manifold: a locally compact manifold must be modelled on a locally compact space.
FiniteDimensional.of_locallyCompact_manifold: a locally compact manifolds must be modelled on a finite-dimensional space

def PartialHomeomorph.extend {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners 𝕜 E H) :

PartialEquiv M E

Given a chart f on a manifold with corners, f.extend I is the extended chart to the model vector space.

Equations

f.extend I = f.trans I.toPartialEquiv

theorem PartialHomeomorph.extend_coe {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

↑(f.extend I) = ↑I ∘ ↑f

theorem PartialHomeomorph.extend_coe_symm {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

↑(f.extend I).symm = ↑f.symm ∘ ↑I.symm

theorem PartialHomeomorph.extend_source {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

(f.extend I).source = f.source

theorem PartialHomeomorph.isOpen_extend_source {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

IsOpen (f.extend I).source

theorem PartialHomeomorph.extend_target {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

(f.extend I).target = ↑I.symm ⁻¹' f.target ∩ Set.range ↑I

theorem PartialHomeomorph.extend_target' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

(f.extend I).target = ↑I '' f.target

theorem PartialHomeomorph.isOpen_extend_target {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] :

IsOpen (f.extend I).target

theorem PartialHomeomorph.mapsTo_extend {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} (hs : s ⊆ f.source) :

Set.MapsTo (↑(f.extend I)) s (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I)

theorem PartialHomeomorph.extend_left_inv {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M} (hxf : x ∈ f.source) :

↑(f.extend I).symm (↑(f.extend I) x) = x

theorem PartialHomeomorph.extend_left_inv' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {t : Set M} (ht : t ⊆ f.source) :

↑(f.extend I).symm ∘ ↑(f.extend I) '' t = t

Variant of f.extend_left_inv I, stated in terms of images.

theorem PartialHomeomorph.extend_source_mem_nhds {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M} (h : x ∈ f.source) :

(f.extend I).source ∈ nhds x

theorem PartialHomeomorph.extend_source_mem_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {x : M} (h : x ∈ f.source) :

(f.extend I).source ∈ nhdsWithin x s

theorem PartialHomeomorph.continuousOn_extend {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

ContinuousOn (↑(f.extend I)) (f.extend I).source

theorem PartialHomeomorph.continuousAt_extend {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M} (h : x ∈ f.source) :

ContinuousAt (↑(f.extend I)) x

theorem PartialHomeomorph.map_extend_nhds {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M} (hy : x ∈ f.source) :

Filter.map (↑(f.extend I)) (nhds x) = nhdsWithin (↑(f.extend I) x) (Set.range ↑I)

theorem PartialHomeomorph.map_extend_nhds_of_mem_interior_range {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M} (hx : x ∈ f.source) (h'x : ↑(f.extend I) x ∈ interior (Set.range ↑I)) :

Filter.map (↑(f.extend I)) (nhds x) = nhds (↑(f.extend I) x)

theorem PartialHomeomorph.map_extend_nhds_of_boundaryless {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {x : M} (hx : x ∈ f.source) :

Filter.map (↑(f.extend I)) (nhds x) = nhds (↑(f.extend I) x)

theorem PartialHomeomorph.extend_target_mem_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {y : M} (hy : y ∈ f.source) :

(f.extend I).target ∈ nhdsWithin (↑(f.extend I) y) (Set.range ↑I)

theorem PartialHomeomorph.extend_image_target_mem_nhds {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M} (hx : x ∈ f.source) :

↑I '' f.target ∈ nhdsWithin (↑(f.extend I) x) (Set.range ↑I)

theorem PartialHomeomorph.extend_image_nhds_mem_nhds_of_boundaryless {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {x : M} (hx : x ∈ f.source) {s : Set M} (h : s ∈ nhds x) :

↑(f.extend I) '' s ∈ nhds (↑(f.extend I) x)

@[deprecated PartialHomeomorph.extend_image_nhds_mem_nhds_of_boundaryless (since := "2025-05-22")]

theorem PartialHomeomorph.extend_image_nhd_mem_nhds_of_boundaryless {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {x : M} (hx : x ∈ f.source) {s : Set M} (h : s ∈ nhds x) :

↑(f.extend I) '' s ∈ nhds (↑(f.extend I) x)

Alias of PartialHomeomorph.extend_image_nhds_mem_nhds_of_boundaryless.

theorem PartialHomeomorph.extend_image_nhds_mem_nhds_of_mem_interior_range {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M} (hx : x ∈ f.source) (h'x : ↑(f.extend I) x ∈ interior (Set.range ↑I)) {s : Set M} (h : s ∈ nhds x) :

↑(f.extend I) '' s ∈ nhds (↑(f.extend I) x)

@[deprecated PartialHomeomorph.extend_image_nhds_mem_nhds_of_mem_interior_range (since := "2025-05-22")]

theorem PartialHomeomorph.extend_image_nhd_mem_nhds_of_mem_interior_range {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M} (hx : x ∈ f.source) (h'x : ↑(f.extend I) x ∈ interior (Set.range ↑I)) {s : Set M} (h : s ∈ nhds x) :

↑(f.extend I) '' s ∈ nhds (↑(f.extend I) x)

Alias of PartialHomeomorph.extend_image_nhds_mem_nhds_of_mem_interior_range.

theorem PartialHomeomorph.extend_target_subset_range {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

(f.extend I).target ⊆ Set.range ↑I

theorem PartialHomeomorph.interior_extend_target_subset_interior_range {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

interior (f.extend I).target ⊆ interior (Set.range ↑I)

theorem PartialHomeomorph.mem_interior_extend_target {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {y : H} (hy : y ∈ f.target) (hy' : ↑I y ∈ interior (Set.range ↑I)) :

↑I y ∈ interior (f.extend I).target

If y ∈ f.target and I y ∈ interior (range I), then I y is an interior point of (I ∘ f).target.

theorem PartialHomeomorph.nhdsWithin_extend_target_eq {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {y : M} (hy : y ∈ f.source) :

nhdsWithin (↑(f.extend I) y) (f.extend I).target = nhdsWithin (↑(f.extend I) y) (Set.range ↑I)

theorem PartialHomeomorph.extend_target_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {y : M} (hy : y ∈ f.source) :

(f.extend I).target =ᶠ[nhds (↑(f.extend I) y)] Set.range ↑I

theorem PartialHomeomorph.continuousAt_extend_symm' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : E} (h : x ∈ (f.extend I).target) :

ContinuousAt (↑(f.extend I).symm) x

theorem PartialHomeomorph.continuousAt_extend_symm {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M} (h : x ∈ f.source) :

ContinuousAt (↑(f.extend I).symm) (↑(f.extend I) x)

theorem PartialHomeomorph.continuousOn_extend_symm {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

ContinuousOn (↑(f.extend I).symm) (f.extend I).target

theorem PartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {X : Type u_8} [TopologicalSpace X] {g : M → X} {s : Set M} {x : M} :

ContinuousWithinAt (g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I) (↑(f.extend I) x) ↔ ContinuousWithinAt (g ∘ ↑f.symm) (↑f.symm ⁻¹' s) (↑f x)

theorem PartialHomeomorph.isOpen_extend_preimage' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set E} (hs : IsOpen s) :

IsOpen ((f.extend I).source ∩ ↑(f.extend I) ⁻¹' s)

theorem PartialHomeomorph.isOpen_extend_preimage {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set E} (hs : IsOpen s) :

IsOpen (f.source ∩ ↑(f.extend I) ⁻¹' s)

theorem PartialHomeomorph.map_extend_nhdsWithin_eq_image {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {y : M} (hy : y ∈ f.source) :

Filter.map (↑(f.extend I)) (nhdsWithin y s) = nhdsWithin (↑(f.extend I) y) (↑(f.extend I) '' ((f.extend I).source ∩ s))

theorem PartialHomeomorph.map_extend_nhdsWithin_eq_image_of_subset {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {y : M} (hy : y ∈ f.source) (hs : s ⊆ f.source) :

Filter.map (↑(f.extend I)) (nhdsWithin y s) = nhdsWithin (↑(f.extend I) y) (↑(f.extend I) '' s)

theorem PartialHomeomorph.map_extend_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {y : M} (hy : y ∈ f.source) :

Filter.map (↑(f.extend I)) (nhdsWithin y s) = nhdsWithin (↑(f.extend I) y) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I)

theorem PartialHomeomorph.map_extend_symm_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {y : M} (hy : y ∈ f.source) :

Filter.map (↑(f.extend I).symm) (nhdsWithin (↑(f.extend I) y) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I)) = nhdsWithin y s

theorem PartialHomeomorph.map_extend_symm_nhdsWithin_range {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {y : M} (hy : y ∈ f.source) :

Filter.map (↑(f.extend I).symm) (nhdsWithin (↑(f.extend I) y) (Set.range ↑I)) = nhds y

theorem PartialHomeomorph.tendsto_extend_comp_iff {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {α : Type u_8} {l : Filter α} {g : α → M} (hg : ∀ᶠ (z : α) in l, g z ∈ f.source) {y : M} (hy : y ∈ f.source) :

Filter.Tendsto (↑(f.extend I) ∘ g) l (nhds (↑(f.extend I) y)) ↔ Filter.Tendsto g l (nhds y)

theorem PartialHomeomorph.continuousWithinAt_writtenInExtend_iff {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] [TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} {s : Set M} {f' : PartialHomeomorph M' H'} {g : M → M'} {y : M} (hy : y ∈ f.source) (hgy : g y ∈ f'.source) (hmaps : Set.MapsTo g s f'.source) :

ContinuousWithinAt (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I) (↑(f.extend I) y) ↔ ContinuousWithinAt g s y

theorem PartialHomeomorph.continuousOn_writtenInExtend_iff {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] [TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} {s : Set M} {f' : PartialHomeomorph M' H'} {g : M → M'} (hs : s ⊆ f.source) (hmaps : Set.MapsTo g s f'.source) :

ContinuousOn (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I) '' s) ↔ ContinuousOn g s

If s ⊆ f.source and g x ∈ f'.source whenever x ∈ s, then g is continuous on s if and only if g written in charts f.extend I and f'.extend I' is continuous on f.extend I '' s.

theorem PartialHomeomorph.extend_preimage_mem_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s t : Set M} {x : M} (h : x ∈ f.source) (ht : t ∈ nhdsWithin x s) :

↑(f.extend I).symm ⁻¹' t ∈ nhdsWithin (↑(f.extend I) x) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I)

Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point in the source is a neighborhood of the preimage, within a set.

theorem PartialHomeomorph.extend_preimage_mem_nhds {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {t : Set M} {x : M} (h : x ∈ f.source) (ht : t ∈ nhds x) :

↑(f.extend I).symm ⁻¹' t ∈ nhds (↑(f.extend I) x)

theorem PartialHomeomorph.extend_preimage_inter_eq {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s t : Set M} :

↑(f.extend I).symm ⁻¹' (s ∩ t) ∩ Set.range ↑I = ↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I ∩ ↑(f.extend I).symm ⁻¹' t

Technical lemma to rewrite suitably the preimage of an intersection under an extended chart, to bring it into a convenient form to apply derivative lemmas.

theorem PartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq_aux {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {x : M} (hx : x ∈ f.source) :

↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I =ᶠ[nhds (↑(f.extend I) x)] (f.extend I).target ∩ ↑(f.extend I).symm ⁻¹' s

theorem PartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {x : M} (hs : s ⊆ f.source) (hx : x ∈ f.source) :

↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I =ᶠ[nhds (↑(f.extend I) x)] ↑(f.extend I) '' s

We use the name extend_coord_change for (f'.extend I).symm ≫ f.extend I.

theorem PartialHomeomorph.extend_coord_change_source {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f f' : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

((f.extend I).symm.trans (f'.extend I)).source = ↑I '' (f.symm.trans f').source

theorem PartialHomeomorph.extend_image_source_inter {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f f' : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} :

↑(f.extend I) '' (f.source ∩ f'.source) = ((f.extend I).symm.trans (f'.extend I)).source

theorem PartialHomeomorph.extend_coord_change_source_mem_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f f' : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : E} (hx : x ∈ ((f.extend I).symm.trans (f'.extend I)).source) :

((f.extend I).symm.trans (f'.extend I)).source ∈ nhdsWithin x (Set.range ↑I)

theorem PartialHomeomorph.extend_coord_change_source_mem_nhdsWithin' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f f' : PartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M} (hxf : x ∈ f.source) (hxf' : x ∈ f'.source) :

((f.extend I).symm.trans (f'.extend I)).source ∈ nhdsWithin (↑(f.extend I) x) (Set.range ↑I)

theorem PartialHomeomorph.contDiffOn_extend_coord_change {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {n : WithTop ℕ∞} {f f' : PartialHomeomorph M H} {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (hf : f ∈ IsManifold.maximalAtlas I n M) (hf' : f' ∈ IsManifold.maximalAtlas I n M) :

ContDiffOn 𝕜 n (↑(f.extend I) ∘ ↑(f'.extend I).symm) ((f'.extend I).symm.trans (f.extend I)).source

theorem PartialHomeomorph.contDiffWithinAt_extend_coord_change {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {n : WithTop ℕ∞} {f f' : PartialHomeomorph M H} {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (hf : f ∈ IsManifold.maximalAtlas I n M) (hf' : f' ∈ IsManifold.maximalAtlas I n M) {x : E} (hx : x ∈ ((f'.extend I).symm.trans (f.extend I)).source) :

ContDiffWithinAt 𝕜 n (↑(f.extend I) ∘ ↑(f'.extend I).symm) (Set.range ↑I) x

theorem PartialHomeomorph.contDiffWithinAt_extend_coord_change' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {n : WithTop ℕ∞} {f f' : PartialHomeomorph M H} {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (hf : f ∈ IsManifold.maximalAtlas I n M) (hf' : f' ∈ IsManifold.maximalAtlas I n M) {x : M} (hxf : x ∈ f.source) (hxf' : x ∈ f'.source) :

ContDiffWithinAt 𝕜 n (↑(f.extend I) ∘ ↑(f'.extend I).symm) (Set.range ↑I) (↑(f'.extend I) x)

def extChartAt {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (I : ModelWithCorners 𝕜 E H) [ChartedSpace H M] (x : M) :

PartialEquiv M E

The preferred extended chart on a manifold with corners around a point x, from a neighborhood of x to the model vector space.

Equations

extChartAt I x = (chartAt H x).extend I

theorem extChartAt_coe {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

↑(extChartAt I x) = ↑I ∘ ↑(chartAt H x)

theorem extChartAt_coe_symm {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

↑(extChartAt I x).symm = ↑(chartAt H x).symm ∘ ↑I.symm

theorem extChartAt_source {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (I : ModelWithCorners 𝕜 E H) [ChartedSpace H M] (x : M) :

(extChartAt I x).source = (chartAt H x).source

theorem isOpen_extChartAt_source {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

IsOpen (extChartAt I x).source

theorem mem_extChartAt_source {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

x ∈ (extChartAt I x).source

theorem mem_extChartAt_target {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

↑(extChartAt I x) x ∈ (extChartAt I x).target

theorem extChartAt_target {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (I : ModelWithCorners 𝕜 E H) [ChartedSpace H M] (x : M) :

(extChartAt I x).target = ↑I.symm ⁻¹' (chartAt H x).target ∩ Set.range ↑I

theorem uniqueDiffOn_extChartAt_target {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

UniqueDiffOn 𝕜 (extChartAt I x).target

theorem uniqueDiffWithinAt_extChartAt_target {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

UniqueDiffWithinAt 𝕜 (extChartAt I x).target (↑(extChartAt I x) x)

theorem extChartAt_to_inv {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

↑(extChartAt I x).symm (↑(extChartAt I x) x) = x

theorem mapsTo_extChartAt {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] {x : M} (hs : s ⊆ (chartAt H x).source) :

Set.MapsTo (↑(extChartAt I x)) s (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)

theorem extChartAt_source_mem_nhds' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x x' : M} (h : x' ∈ (extChartAt I x).source) :

(extChartAt I x).source ∈ nhds x'

theorem extChartAt_source_mem_nhds {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

(extChartAt I x).source ∈ nhds x

theorem extChartAt_source_mem_nhdsWithin' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] {x x' : M} (h : x' ∈ (extChartAt I x).source) :

(extChartAt I x).source ∈ nhdsWithin x' s

theorem extChartAt_source_mem_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] (x : M) :

(extChartAt I x).source ∈ nhdsWithin x s

theorem continuousOn_extChartAt {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

ContinuousOn (↑(extChartAt I x)) (extChartAt I x).source

theorem continuousAt_extChartAt' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x x' : M} (h : x' ∈ (extChartAt I x).source) :

ContinuousAt (↑(extChartAt I x)) x'

theorem continuousAt_extChartAt {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

ContinuousAt (↑(extChartAt I x)) x

theorem map_extChartAt_nhds' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x y : M} (hy : y ∈ (extChartAt I x).source) :

Filter.map (↑(extChartAt I x)) (nhds y) = nhdsWithin (↑(extChartAt I x) y) (Set.range ↑I)

theorem map_extChartAt_nhds {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

Filter.map (↑(extChartAt I x)) (nhds x) = nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I)

theorem map_extChartAt_nhds_of_boundaryless {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] [I.Boundaryless] (x : M) :

Filter.map (↑(extChartAt I x)) (nhds x) = nhds (↑(extChartAt I x) x)

theorem extChartAt_image_nhds_mem_nhds_of_mem_interior_range {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x y : M} (hx : y ∈ (extChartAt I x).source) (h'x : ↑(extChartAt I x) y ∈ interior (Set.range ↑I)) {s : Set M} (h : s ∈ nhds y) :

↑(extChartAt I x) '' s ∈ nhds (↑(extChartAt I x) y)

@[deprecated extChartAt_image_nhds_mem_nhds_of_mem_interior_range (since := "2025-05-22")]

theorem extChartAt_image_nhd_mem_nhds_of_mem_interior_range {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x y : M} (hx : y ∈ (extChartAt I x).source) (h'x : ↑(extChartAt I x) y ∈ interior (Set.range ↑I)) {s : Set M} (h : s ∈ nhds y) :

↑(extChartAt I x) '' s ∈ nhds (↑(extChartAt I x) y)

Alias of extChartAt_image_nhds_mem_nhds_of_mem_interior_range.

theorem extChartAt_image_nhds_mem_nhds_of_boundaryless {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] [I.Boundaryless] {x : M} (hx : s ∈ nhds x) :

↑(extChartAt I x) '' s ∈ nhds (↑(extChartAt I x) x)

@[deprecated extChartAt_image_nhds_mem_nhds_of_boundaryless (since := "2025-05-22")]

theorem extChartAt_image_nhd_mem_nhds_of_boundaryless {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] [I.Boundaryless] {x : M} (hx : s ∈ nhds x) :

↑(extChartAt I x) '' s ∈ nhds (↑(extChartAt I x) x)

Alias of extChartAt_image_nhds_mem_nhds_of_boundaryless.

theorem extChartAt_target_mem_nhdsWithin' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x y : M} (hy : y ∈ (extChartAt I x).source) :

(extChartAt I x).target ∈ nhdsWithin (↑(extChartAt I x) y) (Set.range ↑I)

theorem extChartAt_target_mem_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

(extChartAt I x).target ∈ nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I)

theorem extChartAt_target_mem_nhdsWithin_of_mem {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x : M} {y : E} (hy : y ∈ (extChartAt I x).target) :

(extChartAt I x).target ∈ nhdsWithin y (Set.range ↑I)

theorem extChartAt_target_union_compl_range_mem_nhds_of_mem {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {y : E} {x : M} (hy : y ∈ (extChartAt I x).target) :

(extChartAt I x).target ∪ (Set.range ↑I)ᶜ ∈ nhds y

@[deprecated extChartAt_target_union_compl_range_mem_nhds_of_mem (since := "2024-11-27")]

theorem extChartAt_target_union_comp_range_mem_nhds_of_mem {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {y : E} {x : M} (hy : y ∈ (extChartAt I x).target) :

(extChartAt I x).target ∪ (Set.range ↑I)ᶜ ∈ nhds y

Alias of extChartAt_target_union_compl_range_mem_nhds_of_mem.

theorem isOpen_extChartAt_target {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] [I.Boundaryless] (x : M) :

IsOpen (extChartAt I x).target

If we're boundaryless, extChartAt has open target

theorem extChartAt_target_mem_nhds {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] [I.Boundaryless] (x : M) :

(extChartAt I x).target ∈ nhds (↑(extChartAt I x) x)

If we're boundaryless, (extChartAt I x).target is a neighborhood of the key point

theorem extChartAt_target_mem_nhds' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] [I.Boundaryless] {x : M} {y : E} (m : y ∈ (extChartAt I x).target) :

(extChartAt I x).target ∈ nhds y

If we're boundaryless, (extChartAt I x).target is a neighborhood of any of its points

theorem extChartAt_target_subset_range {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

(extChartAt I x).target ⊆ Set.range ↑I

theorem nhdsWithin_extChartAt_target_eq' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x y : M} (hy : y ∈ (extChartAt I x).source) :

nhdsWithin (↑(extChartAt I x) y) (extChartAt I x).target = nhdsWithin (↑(extChartAt I x) y) (Set.range ↑I)

Around the image of a point in the source, the neighborhoods are the same within (extChartAt I x).target and within range I.

theorem nhdsWithin_extChartAt_target_eq_of_mem {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x : M} {z : E} (hz : z ∈ (extChartAt I x).target) :

nhdsWithin z (extChartAt I x).target = nhdsWithin z (Set.range ↑I)

Around a point in the target, the neighborhoods are the same within (extChartAt I x).target and within range I.

theorem nhdsWithin_extChartAt_target_eq {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

nhdsWithin (↑(extChartAt I x) x) (extChartAt I x).target = nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I)

Around the image of the base point, the neighborhoods are the same within (extChartAt I x).target and within range I.

theorem extChartAt_target_eventuallyEq' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x y : M} (hy : y ∈ (extChartAt I x).source) :

(extChartAt I x).target =ᶠ[nhds (↑(extChartAt I x) y)] Set.range ↑I

Around the image of a point in the source, (extChartAt I x).target and range I coincide locally.

theorem extChartAt_target_eventuallyEq_of_mem {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x : M} {z : E} (hz : z ∈ (extChartAt I x).target) :

(extChartAt I x).target =ᶠ[nhds z] Set.range ↑I

Around a point in the target, (extChartAt I x).target and range I coincide locally.

theorem extChartAt_target_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x : M} :

(extChartAt I x).target =ᶠ[nhds (↑(extChartAt I x) x)] Set.range ↑I

Around the image of the base point, (extChartAt I x).target and range I coincide locally.

theorem continuousAt_extChartAt_symm'' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :

ContinuousAt (↑(extChartAt I x).symm) y

theorem continuousAt_extChartAt_symm' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x x' : M} (h : x' ∈ (extChartAt I x).source) :

ContinuousAt (↑(extChartAt I x).symm) (↑(extChartAt I x) x')

theorem continuousAt_extChartAt_symm {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

ContinuousAt (↑(extChartAt I x).symm) (↑(extChartAt I x) x)

theorem continuousOn_extChartAt_symm {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

ContinuousOn (↑(extChartAt I x).symm) (extChartAt I x).target

theorem extChartAt_target_subset_closure_interior {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x : M} :

(extChartAt I x).target ⊆ closure (interior (extChartAt I x).target)

theorem interior_extChartAt_target_nonempty {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (I : ModelWithCorners 𝕜 E H) [ChartedSpace H M] (x : M) :

(interior (extChartAt I x).target).Nonempty

theorem extChartAt_mem_closure_interior {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] {x₀ x : M} (hx : x ∈ closure (interior s)) (h'x : x ∈ (extChartAt I x₀).source) :

↑(extChartAt I x₀) x ∈ closure (interior (↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target))

theorem isOpen_extChartAt_preimage' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) {s : Set E} (hs : IsOpen s) :

IsOpen ((extChartAt I x).source ∩ ↑(extChartAt I x) ⁻¹' s)

theorem isOpen_extChartAt_preimage {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) {s : Set E} (hs : IsOpen s) :

IsOpen ((chartAt H x).source ∩ ↑(extChartAt I x) ⁻¹' s)

theorem map_extChartAt_nhdsWithin_eq_image' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] {x y : M} (hy : y ∈ (extChartAt I x).source) :

Filter.map (↑(extChartAt I x)) (nhdsWithin y s) = nhdsWithin (↑(extChartAt I x) y) (↑(extChartAt I x) '' ((extChartAt I x).source ∩ s))

theorem map_extChartAt_nhdsWithin_eq_image {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] (x : M) :

Filter.map (↑(extChartAt I x)) (nhdsWithin x s) = nhdsWithin (↑(extChartAt I x) x) (↑(extChartAt I x) '' ((extChartAt I x).source ∩ s))

theorem map_extChartAt_nhdsWithin' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] {x y : M} (hy : y ∈ (extChartAt I x).source) :

Filter.map (↑(extChartAt I x)) (nhdsWithin y s) = nhdsWithin (↑(extChartAt I x) y) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)

theorem map_extChartAt_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] (x : M) :

Filter.map (↑(extChartAt I x)) (nhdsWithin x s) = nhdsWithin (↑(extChartAt I x) x) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)

theorem map_extChartAt_symm_nhdsWithin' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] {x y : M} (hy : y ∈ (extChartAt I x).source) :

Filter.map (↑(extChartAt I x).symm) (nhdsWithin (↑(extChartAt I x) y) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)) = nhdsWithin y s

theorem map_extChartAt_symm_nhdsWithin_range' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x y : M} (hy : y ∈ (extChartAt I x).source) :

Filter.map (↑(extChartAt I x).symm) (nhdsWithin (↑(extChartAt I x) y) (Set.range ↑I)) = nhds y

theorem map_extChartAt_symm_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s : Set M} [ChartedSpace H M] (x : M) :

Filter.map (↑(extChartAt I x).symm) (nhdsWithin (↑(extChartAt I x) x) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)) = nhdsWithin x s

theorem map_extChartAt_symm_nhdsWithin_range {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) :

Filter.map (↑(extChartAt I x).symm) (nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I)) = nhds x

theorem extChartAt_preimage_mem_nhdsWithin' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s t : Set M} [ChartedSpace H M] {x x' : M} (h : x' ∈ (extChartAt I x).source) (ht : t ∈ nhdsWithin x' s) :

↑(extChartAt I x).symm ⁻¹' t ∈ nhdsWithin (↑(extChartAt I x) x') (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)

Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point in the source is a neighborhood of the preimage, within a set.

theorem extChartAt_preimage_mem_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s t : Set M} [ChartedSpace H M] {x : M} (ht : t ∈ nhdsWithin x s) :

↑(extChartAt I x).symm ⁻¹' t ∈ nhdsWithin (↑(extChartAt I x) x) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)

Technical lemma ensuring that the preimage under an extended chart of a neighborhood of the base point is a neighborhood of the preimage, within a set.

theorem extChartAt_preimage_mem_nhds' {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {t : Set M} [ChartedSpace H M] {x x' : M} (h : x' ∈ (extChartAt I x).source) (ht : t ∈ nhds x') :

↑(extChartAt I x).symm ⁻¹' t ∈ nhds (↑(extChartAt I x) x')

theorem extChartAt_preimage_mem_nhds {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {t : Set M} [ChartedSpace H M] {x : M} (ht : t ∈ nhds x) :

↑(extChartAt I x).symm ⁻¹' t ∈ nhds (↑(extChartAt I x) x)

Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point is a neighborhood of the preimage.

theorem extChartAt_preimage_inter_eq {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {s t : Set M} [ChartedSpace H M] (x : M) :

↑(extChartAt I x).symm ⁻¹' (s ∩ t) ∩ Set.range ↑I = ↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' t

Technical lemma to rewrite suitably the preimage of an intersection under an extended chart, to bring it into a convenient form to apply derivative lemmas.

theorem ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] [TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} {s : Set M} [ChartedSpace H M] [ChartedSpace H' M'] {f : M → M'} {x : M} (hc : ContinuousWithinAt f s x) :

nhdsWithin (↑(extChartAt I x) x) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) = nhdsWithin (↑(extChartAt I x) x) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))

theorem ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] [TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} {s : Set M} [ChartedSpace H M] [ChartedSpace H' M'] {f : M → M'} {x : M} (hc : ContinuousWithinAt f s x) :

↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I =ᶠ[nhds (↑(extChartAt I x) x)] (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

We use the name ext_coord_change for (extChartAt I x').symm ≫ extChartAt I x.

theorem ext_coord_change_source {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x x' : M) :

((extChartAt I x').symm.trans (extChartAt I x)).source = ↑I '' ((chartAt H x').symm.trans (chartAt H x)).source

theorem contDiffOn_ext_coord_change {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] [IsManifold I n M] (x x' : M) :

ContDiffOn 𝕜 n (↑(extChartAt I x) ∘ ↑(extChartAt I x').symm) ((extChartAt I x').symm.trans (extChartAt I x)).source

theorem contDiffWithinAt_ext_coord_change {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] [IsManifold I n M] (x x' : M) {y : E} (hy : y ∈ ((extChartAt I x').symm.trans (extChartAt I x)).source) :

ContDiffWithinAt 𝕜 n (↑(extChartAt I x) ∘ ↑(extChartAt I x').symm) (Set.range ↑I) y

def writtenInExtChartAt {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (I : ModelWithCorners 𝕜 E H) [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] [TopologicalSpace M'] (I' : ModelWithCorners 𝕜 E' H') [ChartedSpace H M] [ChartedSpace H' M'] (x : M) (f : M → M') :

E → E'

Conjugating a function to write it in the preferred charts around x. The manifold derivative of f will just be the derivative of this conjugated function.

Equations

writtenInExtChartAt I I' x f = ↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm

theorem writtenInExtChartAt_chartAt {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :

writtenInExtChartAt I I x (↑(chartAt H x)) y = y

theorem writtenInExtChartAt_chartAt_symm {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :

writtenInExtChartAt I I (↑(chartAt H x) x) (↑(chartAt H x).symm) y = y

theorem writtenInExtChartAt_extChartAt {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :

writtenInExtChartAt I (modelWithCornersSelf 𝕜 E) x (↑(extChartAt I x)) y = y

theorem writtenInExtChartAt_extChartAt_symm {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :

writtenInExtChartAt (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x) x) (↑(extChartAt I x).symm) y = y

theorem extChartAt_self_eq (𝕜 : Type u_1) {E : Type u_2} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {x : H} :

↑(extChartAt I x) = ↑I

theorem extChartAt_self_apply (𝕜 : Type u_1) {E : Type u_2} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {x y : H} :

↑(extChartAt I x) y = ↑I y

theorem extChartAt_model_space_eq_id (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) :

extChartAt (modelWithCornersSelf 𝕜 E) x = PartialEquiv.refl E

In the case of the manifold structure on a vector space, the extended charts are just the identity.

theorem ext_chart_model_space_apply (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x y : E} :

↑(extChartAt (modelWithCornersSelf 𝕜 E) x) y = y

theorem extChartAt_prod {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] [TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} [ChartedSpace H M] [ChartedSpace H' M'] (x : M × M') :

extChartAt (I.prod I') x = (extChartAt I x.1).prod (extChartAt I' x.2)

theorem extChartAt_comp {𝕜 : Type u_1} {E : Type u_2} {H : Type u_4} {M' : Type u_6} {H' : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] [ChartedSpace H H'] (x : M') :

extChartAt I x = (chartAt H' x).trans (extChartAt I (↑(chartAt H' x) x))

theorem writtenInExtChartAt_chartAt_comp {𝕜 : Type u_1} {E : Type u_2} {H : Type u_4} {M' : Type u_6} {H' : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] [ChartedSpace H H'] (x : M') {y : E} (hy : y ∈ (extChartAt I x).target) :

writtenInExtChartAt I I x (↑(chartAt H' x)) y = y

theorem writtenInExtChartAt_chartAt_symm_comp {𝕜 : Type u_1} {E : Type u_2} {H : Type u_4} {M' : Type u_6} {H' : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] [ChartedSpace H H'] (x : M') {y : E} (hy : y ∈ (extChartAt I x).target) :

writtenInExtChartAt I I (↑(chartAt H' x) x) (↑(chartAt H' x).symm) y = y

theorem Manifold.locallyCompact_of_finiteDimensional {E : Type u_8} {𝕜 : Type u_9} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_10} [TopologicalSpace H] {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners 𝕜 E H) [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E] :

LocallyCompactSpace M

A finite-dimensional manifold modelled on a locally compact field (such as ℝ, ℂ or the p-adic numbers) is locally compact.

theorem LocallyCompactSpace.of_locallyCompact_manifold {E : Type u_8} {𝕜 : Type u_9} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_10} [TopologicalSpace H] (M : Type u_11) [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners 𝕜 E H) [h : Nonempty M] [LocallyCompactSpace M] :

LocallyCompactSpace E

A locally compact manifold must be modelled on a locally compact space.

theorem FiniteDimensional.of_locallyCompact_manifold {E : Type u_8} {𝕜 : Type u_9} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_10} [TopologicalSpace H] (M : Type u_11) [TopologicalSpace M] [ChartedSpace H M] [CompleteSpace 𝕜] (I : ModelWithCorners 𝕜 E H) [Nonempty M] [LocallyCompactSpace M] :

FiniteDimensional 𝕜 E

Riesz's theorem applied to manifolds: a locally compact manifolds must be modelled on a finite-dimensional space. This is the converse to Manifold.locallyCompact_of_finiteDimensional.