Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

PartialHomeomorph.extend definition

: PartialEquiv M E

Full source

/-- Given a chart `f` on a manifold with corners, `f.extend I` is the extended chart to the model
vector space. -/
@[simp, mfld_simps]
def extend : PartialEquiv M E :=
  f.toPartialEquiv ≫ I.toPartialEquiv

Extended chart via model embedding

Informal description

Given a chart $f$ on a manifold with corners modeled on $(E, H)$, the extended chart $f.\text{extend}\, I$ is the composition of $f$ with the model embedding $I : H \to E$. This yields a partial equivalence between the manifold $M$ and the model vector space $E$. More precisely, $f.\text{extend}\, I$ is defined as the composition of the partial equivalence $f$ (a chart on $M$) with the partial equivalence $I$ (the model embedding). The resulting partial equivalence maps points in the domain of $f$ to their corresponding points in $E$ via $I \circ f$, and its inverse maps points back via $f^{-1} \circ I^{-1}$.

PartialHomeomorph.extend_coe theorem

: ⇑(f.extend I) = I ∘ f

Full source

theorem extend_coe : ⇑(f.extend I) = I ∘ f :=
  rfl

Extended Chart Function Composition: $f.\text{extend}\, I = I \circ f$

Informal description

The function associated with the extended chart $f.\text{extend}\, I$ is equal to the composition of the model embedding $I$ with the chart $f$, i.e., $f.\text{extend}\, I = I \circ f$.

PartialHomeomorph.extend_coe_symm theorem

: ⇑(f.extend I).symm = f.symm ∘ I.symm

Full source

theorem extend_coe_symm : ⇑(f.extend I).symm = f.symm ∘ I.symm :=
  rfl

Inverse of Extended Chart as Composition of Inverses

Informal description

The inverse of the extended chart $f.\text{extend}\, I$ is equal to the composition of the inverse chart $f^{-1}$ with the inverse model embedding $I^{-1}$, i.e., $(f.\text{extend}\, I)^{-1} = f^{-1} \circ I^{-1}$.

PartialHomeomorph.extend_source theorem

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

Full source

theorem extend_source : (f.extend I).source = f.source := by
  rw [extend, PartialEquiv.trans_source, I.source_eq, preimage_univ, inter_univ]

Source of Extended Chart Equals Source of Original Chart

Informal description

For a partial homeomorphism $f$ on a manifold with corners modeled on $(E, H)$ and a model embedding $I : H \to E$, the source of the extended chart $f.\text{extend}\, I$ equals the source of $f$, i.e., $$\text{source}(f.\text{extend}\, I) = \text{source}(f).$$

PartialHomeomorph.isOpen_extend_source theorem

: IsOpen (f.extend I).source

Full source

theorem isOpen_extend_source : IsOpen (f.extend I).source := by
  rw [extend_source]
  exact f.open_source

Openness of Extended Chart Source

Informal description

For a partial homeomorphism $f$ on a manifold with corners modeled on $(E, H)$ and a model embedding $I : H \to E$, the source of the extended chart $f.\text{extend}\, I$ is an open subset of the manifold $M$.

PartialHomeomorph.extend_target theorem

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

Full source

theorem extend_target : (f.extend I).target = I.symm ⁻¹' f.targetI.symm ⁻¹' f.target ∩ range I := by
  simp_rw [extend, PartialEquiv.trans_target, I.target_eq, I.toPartialEquiv_coe_symm, inter_comm]

Target of Extended Chart as Intersection of Preimage and Range

Informal description

For a partial homeomorphism $f$ on a manifold with corners modeled on $(E, H)$, the target of the extended chart $f.\text{extend}\, I$ is equal to the intersection of the preimage of $f.\text{target}$ under the inverse model embedding $I^{-1}$ and the range of $I$. In other words: $$(f.\text{extend}\, I).\text{target} = I^{-1}(f.\text{target}) \cap \text{range}(I)$$

PartialHomeomorph.extend_target' theorem

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

Full source

theorem extend_target' : (f.extend I).target = I '' f.target := by
  rw [extend, PartialEquiv.trans_target'', I.source_eq, univ_inter, I.toPartialEquiv_coe]

Target of Extended Chart as Image under Model Embedding

Informal description

For a partial homeomorphism $f$ on a manifold with corners modeled on $(E, H)$, the target of the extended chart $f.\text{extend}\, I$ is equal to the image of $f.\text{target}$ under the model embedding $I : H \to E$. In other words: $$(f.\text{extend}\, I).\text{target} = I(f.\text{target}).$$

PartialHomeomorph.isOpen_extend_target theorem

[I.Boundaryless] : IsOpen (f.extend I).target

Full source

lemma isOpen_extend_target [I.Boundaryless] : IsOpen (f.extend I).target := by
  rw [extend_target, I.range_eq_univ, inter_univ]
  exact I.continuous_symm.isOpen_preimage _ f.open_target

Openness of Extended Chart Target for Boundaryless Models

Informal description

For a boundaryless model with corners $I$ embedding a topological space $H$ into a normed vector space $E$, and for any partial homeomorphism $f$ on a manifold modeled on $(E, H)$, the target of the extended chart $f.\text{extend}\, I$ is an open subset of $E$.

PartialHomeomorph.mapsTo_extend theorem

(hs : s ⊆ f.source) : MapsTo (f.extend I) s ((f.extend I).symm ⁻¹' s ∩ range I)

Full source

theorem mapsTo_extend (hs : s ⊆ f.source) :
    MapsTo (f.extend I) s ((f.extend I).symm ⁻¹' s(f.extend I).symm ⁻¹' s ∩ range I) := by
  rw [mapsTo', extend_coe, extend_coe_symm, preimage_comp, ← I.image_eq, image_comp,
    f.image_eq_target_inter_inv_preimage hs]
  exact image_subset _ inter_subset_right

Mapping Property of Extended Charts: $f.\text{extend}\, I$ Preserves Preimage-Range Intersection

Informal description

Let $f$ be a partial homeomorphism from a manifold $M$ to the model space $H$, and let $I$ be a model with corners embedding $H$ into the vector space $E$. For any subset $s \subseteq M$ contained in the source of $f$, the extended chart $f.\text{extend}\, I$ maps $s$ into the intersection of the preimage of $s$ under $(f.\text{extend}\, I)^{-1}$ with the range of $I$. In symbols, if $s \subseteq f.\text{source}$, then: $$ f.\text{extend}\, I(s) \subseteq (f.\text{extend}\, I)^{-1}(s) \cap \text{range}(I). $$

PartialHomeomorph.extend_left_inv theorem

{x : M} (hxf : x ∈ f.source) : (f.extend I).symm (f.extend I x) = x

Full source

theorem extend_left_inv {x : M} (hxf : x ∈ f.source) : (f.extend I).symm (f.extend I x) = x :=
  (f.extend I).left_inv <| by rwa [f.extend_source]

Inverse Property of Extended Chart on Manifold with Corners

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$, and let $f$ be a chart on $M$. For any point $x$ in the source of $f$, the composition of the extended chart $f.\text{extend}\, I$ with its inverse maps $x$ back to itself, i.e., $$(f.\text{extend}\, I)^{-1} \circ (f.\text{extend}\, I)(x) = x.$$

PartialHomeomorph.extend_left_inv' theorem

(ht : t ⊆ f.source) : ((f.extend I).symm ∘ (f.extend I)) '' t = t

Full source

/-- Variant of `f.extend_left_inv I`, stated in terms of images. -/
lemma extend_left_inv' (ht : t ⊆ f.source) : ((f.extend I).symm ∘ (f.extend I)) '' t = t :=
  EqOn.image_eq_self (fun _ hx ↦ f.extend_left_inv (ht hx))

Image Preservation Property of Extended Chart Composition on Manifold Subset

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$, and let $f$ be a chart on $M$. For any subset $t \subseteq f.\text{source}$, the image of $t$ under the composition $(f.\text{extend}\, I)^{-1} \circ (f.\text{extend}\, I)$ equals $t$ itself, i.e., $$(f.\text{extend}\, I)^{-1} \circ (f.\text{extend}\, I)(t) = t.$$

PartialHomeomorph.extend_source_mem_nhds theorem

{x : M} (h : x ∈ f.source) : (f.extend I).source ∈ 𝓝 x

Full source

theorem extend_source_mem_nhds {x : M} (h : x ∈ f.source) : (f.extend I).source ∈ 𝓝 x :=
  (isOpen_extend_source f).mem_nhds <| by rwa [f.extend_source]

Neighborhood Property of Extended Chart Source

Informal description

For any point $x$ in the source of a partial homeomorphism $f$ on a manifold $M$ with corners modeled on $(E, H)$, the source of the extended chart $f.\text{extend}\, I$ is a neighborhood of $x$ in $M$.

PartialHomeomorph.extend_source_mem_nhdsWithin theorem

{x : M} (h : x ∈ f.source) : (f.extend I).source ∈ 𝓝[s] x

Full source

theorem extend_source_mem_nhdsWithin {x : M} (h : x ∈ f.source) : (f.extend I).source ∈ 𝓝[s] x :=
  mem_nhdsWithin_of_mem_nhds <| extend_source_mem_nhds f h

Neighborhood Property of Extended Chart Source Within a Subset

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$, and let $f$ be a chart on $M$. For any point $x$ in the source of $f$ and any subset $s \subseteq M$, the source of the extended chart $f.\text{extend}\, I$ is a neighborhood of $x$ within $s$. In other words, if $x \in f.\text{source}$, then there exists a neighborhood $U$ of $x$ in $M$ such that $U \cap s \subseteq (f.\text{extend}\, I).\text{source}$.

PartialHomeomorph.continuousOn_extend theorem

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

Full source

theorem continuousOn_extend : ContinuousOn (f.extend I) (f.extend I).source := by
  refine I.continuous.comp_continuousOn ?_
  rw [extend_source]
  exact f.continuousOn

Continuity of Extended Chart on Source Set

Informal description

The extended chart $f.\text{extend}\, I$ is continuous on its source set, which equals the source set of the original partial homeomorphism $f$.

PartialHomeomorph.continuousAt_extend theorem

{x : M} (h : x ∈ f.source) : ContinuousAt (f.extend I) x

Full source

theorem continuousAt_extend {x : M} (h : x ∈ f.source) : ContinuousAt (f.extend I) x :=
  (continuousOn_extend f).continuousAt <| extend_source_mem_nhds f h

Continuity of Extended Chart at a Point in its Source

Informal description

For any point $x$ in the source of a partial homeomorphism $f$ on a manifold $M$ with corners modeled on $(E, H)$, the extended chart $f.\text{extend}\, I$ is continuous at $x$. Here, $f.\text{extend}\, I$ denotes the composition of $f$ with the model embedding $I \colon H \to E$, which maps points from the manifold to the model vector space $E$.

PartialHomeomorph.map_extend_nhds theorem

{x : M} (hy : x ∈ f.source) : map (f.extend I) (𝓝 x) = 𝓝[range I] f.extend I x

Full source

theorem map_extend_nhds {x : M} (hy : x ∈ f.source) :
    map (f.extend I) (𝓝 x) = 𝓝[range I] f.extend I x := by
  rwa [extend_coe, comp_apply, ← I.map_nhds_eq, ← f.map_nhds_eq, map_map]

Neighborhood Filter Preservation under Extended Chart

Informal description

For any point $x$ in the source of the chart $f$ on a manifold $M$ modeled on $(E, H)$, the pushforward of the neighborhood filter $\mathcal{N}(x)$ under the extended chart $f.\text{extend}\, I$ equals the neighborhood filter of $(f.\text{extend}\, I)(x)$ restricted to the range of the model embedding $I$. In other words: $$ (f.\text{extend}\, I)_*(\mathcal{N}(x)) = \mathcal{N}_{(f.\text{extend}\, I)(x)}|_{\text{range}(I)} $$ where $f.\text{extend}\, I = I \circ f$ is the composition of the chart $f$ with the model embedding $I \colon H \to E$.

PartialHomeomorph.map_extend_nhds_of_mem_interior_range theorem

 {x : M} (hx : x ∈ f.source) (h'x : f.extend I x ∈ interior (range I)) : map (f.extend I) (𝓝 x) = 𝓝 (f.extend I x)

Full source

theorem map_extend_nhds_of_mem_interior_range {x : M} (hx : x ∈ f.source)
    (h'x : f.extend I x ∈ interior (range I)) :
    map (f.extend I) (𝓝 x) = 𝓝 (f.extend I x) := by
  rw [f.map_extend_nhds hx, nhdsWithin_eq_nhds]
  exact mem_of_superset (isOpen_interior.mem_nhds h'x) interior_subset

Neighborhood Filter Preservation under Extended Chart for Interior Points

Informal description

For a point $x$ in the source of a chart $f$ on a manifold $M$ modeled on $(E, H)$, if the image of $x$ under the extended chart $f.\text{extend}\, I$ lies in the interior of the range of the model embedding $I \colon H \to E$, then the pushforward of the neighborhood filter $\mathcal{N}(x)$ under $f.\text{extend}\, I$ equals the full neighborhood filter of $(f.\text{extend}\, I)(x)$ in $E$. In other words, if $x \in f.\text{source}$ and $f.\text{extend}\, I(x) \in \text{interior}(\text{range}(I))$, then: $$ (f.\text{extend}\, I)_*(\mathcal{N}(x)) = \mathcal{N}(f.\text{extend}\, I(x)). $$

PartialHomeomorph.map_extend_nhds_of_boundaryless theorem

[I.Boundaryless] {x : M} (hx : x ∈ f.source) : map (f.extend I) (𝓝 x) = 𝓝 (f.extend I x)

Full source

theorem map_extend_nhds_of_boundaryless [I.Boundaryless] {x : M} (hx : x ∈ f.source) :
    map (f.extend I) (𝓝 x) = 𝓝 (f.extend I x) := by
  rw [f.map_extend_nhds hx, I.range_eq_univ, nhdsWithin_univ]

Neighborhood Filter Preservation under Extended Chart for Boundaryless Models

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$ with boundaryless model $I$, and let $f$ be a chart on $M$. For any point $x$ in the source of $f$, the pushforward of the neighborhood filter $\mathcal{N}(x)$ under the extended chart $f.\text{extend}\, I$ equals the neighborhood filter of $(f.\text{extend}\, I)(x)$. In other words: $$ (f.\text{extend}\, I)_*(\mathcal{N}(x)) = \mathcal{N}((f.\text{extend}\, I)(x)) $$ where $f.\text{extend}\, I = I \circ f$ is the composition of the chart $f$ with the model embedding $I \colon H \to E$.

PartialHomeomorph.extend_target_mem_nhdsWithin theorem

{y : M} (hy : y ∈ f.source) : (f.extend I).target ∈ 𝓝[range I] f.extend I y

Full source

theorem extend_target_mem_nhdsWithin {y : M} (hy : y ∈ f.source) :
    (f.extend I).target ∈ 𝓝[range I] f.extend I y := by
  rw [← PartialEquiv.image_source_eq_target, ← map_extend_nhds f hy]
  exact image_mem_map (extend_source_mem_nhds _ hy)

Neighborhood Property of Extended Chart Target Within Range

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$ with model embedding $I : H \to E$, and let $f$ be a chart on $M$. For any point $y$ in the source of $f$, the target of the extended chart $f.\text{extend}\, I$ is a neighborhood of $(f.\text{extend}\, I)(y)$ within the range of $I$. In other words: $$ (f.\text{extend}\, I).\text{target} \in \mathcal{N}_{(I \circ f)(y)}|_{\text{range}(I)} $$ where $f.\text{extend}\, I = I \circ f$ is the extended chart.

PartialHomeomorph.extend_image_target_mem_nhds theorem

{x : M} (hx : x ∈ f.source) : I '' f.target ∈ 𝓝[range I] (f.extend I) x

Full source

lemma extend_image_target_mem_nhds {x : M} (hx : x ∈ f.source) :
    I '' f.targetI '' f.target ∈ 𝓝[range I] (f.extend I) x := by
  rw [← f.map_extend_nhds hx, Filter.mem_map,
    f.extend_coe, Set.preimage_comp, I.preimage_image f.target]
  exact (f.continuousAt hx).preimage_mem_nhds (f.open_target.mem_nhds (f.map_source hx))

Neighborhood Property of Extended Chart Target Image: $I(f.\text{target})$ is a Neighborhood Within Range of $I$

Informal description

Let $M$ be a manifold with corners modeled on $(E,H)$, $I : H \to E$ be a model with corners, and $f$ be a chart on $M$. For any point $x$ in the source of $f$, the image of $f$'s target under $I$ is a neighborhood of $(f.\text{extend}\, I)(x)$ within the range of $I$, i.e., $$ I(f.\text{target}) \in \mathcal{N}_{(I \circ f)(x)}|_{\text{range}(I)} $$ where $f.\text{extend}\, I = I \circ f$ is the extended chart.

PartialHomeomorph.extend_image_nhd_mem_nhds_of_boundaryless theorem

[I.Boundaryless] {x} (hx : x ∈ f.source) {s : Set M} (h : s ∈ 𝓝 x) : (f.extend I) '' s ∈ 𝓝 ((f.extend I) x)

Full source

theorem extend_image_nhd_mem_nhds_of_boundaryless [I.Boundaryless] {x} (hx : x ∈ f.source)
    {s : Set M} (h : s ∈ 𝓝 x) : (f.extend I) '' s(f.extend I) '' s ∈ 𝓝 ((f.extend I) x) := by
  rw [← f.map_extend_nhds_of_boundaryless hx, Filter.mem_map]
  filter_upwards [h] using subset_preimage_image (f.extend I) s

Neighborhood preservation under extended charts for boundaryless models

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$ with a boundaryless model $I \colon H \to E$, and let $f$ be a chart on $M$. For any point $x$ in the source of $f$ and any neighborhood $s$ of $x$ in $M$, the image of $s$ under the extended chart $f.\text{extend}\, I = I \circ f$ is a neighborhood of $(I \circ f)(x)$ in $E$.

PartialHomeomorph.extend_image_nhd_mem_nhds_of_mem_interior_range theorem

 {x} (hx : x ∈ f.source) (h'x : f.extend I x ∈ interior (range I)) {s : Set M} (h : s ∈ 𝓝 x) :
  (f.extend I) '' s ∈ 𝓝 ((f.extend I) x)

Full source

theorem extend_image_nhd_mem_nhds_of_mem_interior_range {x} (hx : x ∈ f.source)
    (h'x : f.extend I x ∈ interior (range I)) {s : Set M} (h : s ∈ 𝓝 x) :
    (f.extend I) '' s(f.extend I) '' s ∈ 𝓝 ((f.extend I) x) := by
  rw [← f.map_extend_nhds_of_mem_interior_range hx h'x, Filter.mem_map]
  filter_upwards [h] using subset_preimage_image (f.extend I) s

Neighborhood Preservation under Extended Chart for Interior Points

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$, and let $f$ be a chart on $M$ with model embedding $I \colon H \to E$. For a point $x$ in the source of $f$ such that the extended chart value $f.\text{extend}\, I(x)$ lies in the interior of the range of $I$, and for any neighborhood $s$ of $x$ in $M$, the image of $s$ under the extended chart $f.\text{extend}\, I$ is a neighborhood of $f.\text{extend}\, I(x)$ in $E$. In other words, if $x \in f.\text{source}$ and $f.\text{extend}\, I(x) \in \text{interior}(\text{range}(I))$, then for any $s \in \mathcal{N}(x)$, we have: $$ (f.\text{extend}\, I)(s) \in \mathcal{N}((f.\text{extend}\, I)(x)). $$

PartialHomeomorph.extend_target_subset_range theorem

: (f.extend I).target ⊆ range I

Full source

theorem extend_target_subset_range : (f.extend I).target ⊆ range I := by simp only [mfld_simps]

Extended Chart Target Subset of Model Range

Informal description

For any partial homeomorphism $f$ on a manifold $M$ with model $I \colon H \to E$, the target of the extended chart $f.\text{extend}\, I$ is a subset of the range of $I$. In other words, $(f.\text{extend}\, I).\text{target} \subseteq \text{range}(I)$.

PartialHomeomorph.interior_extend_target_subset_interior_range theorem

: interior (f.extend I).target ⊆ interior (range I)

Full source

lemma interior_extend_target_subset_interior_range :
    interiorinterior (f.extend I).target ⊆ interior (range I) := by
  rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq]
  exact inter_subset_right

Interior of Extended Chart Target is Subset of Interior of Model Range

Informal description

For any partial homeomorphism $f$ on a manifold with corners modeled on $(E, H)$, the interior of the target of the extended chart $f.\text{extend}\, I$ is a subset of the interior of the range of the model embedding $I \colon H \to E$, i.e., $$\text{interior}((f.\text{extend}\, I).\text{target}) \subseteq \text{interior}(\text{range}(I)).$$

PartialHomeomorph.mem_interior_extend_target theorem

{y : H} (hy : y ∈ f.target) (hy' : I y ∈ interior (range I)) : I y ∈ interior (f.extend I).target

Full source

/-- If `y ∈ f.target` and `I y ∈ interior (range I)`,
then `I y` is an interior point of `(I ∘ f).target`. -/
lemma mem_interior_extend_target {y : H} (hy : y ∈ f.target)
    (hy' : I y ∈ interior (range I)) : I y ∈ interior (f.extend I).target := by
  rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq,
    mem_inter_iff, mem_preimage]
  exact ⟨mem_of_eq_of_mem (I.left_inv (y)) hy, hy'⟩

Interior Point Preservation under Extended Chart

Informal description

Let $f$ be a partial homeomorphism on a manifold with corners modeled on $(E, H)$, and let $I \colon H \to E$ be the model embedding. For any point $y \in f.\text{target}$ such that $I(y)$ lies in the interior of $\text{range}(I)$, it follows that $I(y)$ is an interior point of $(f.\text{extend}\, I).\text{target}$.

PartialHomeomorph.nhdsWithin_extend_target_eq theorem

{y : M} (hy : y ∈ f.source) : 𝓝[(f.extend I).target] f.extend I y = 𝓝[range I] f.extend I y

Full source

theorem nhdsWithin_extend_target_eq {y : M} (hy : y ∈ f.source) :
    𝓝[(f.extend I).target] f.extend I y = 𝓝[range I] f.extend I y :=
  (nhdsWithin_mono _ (extend_target_subset_range _)).antisymm <|
    nhdsWithin_le_of_mem (extend_target_mem_nhdsWithin _ hy)

Equality of Neighborhood Filters for Extended Chart Target and Model Range

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$ with model embedding $I : H \to E$, and let $f$ be a chart on $M$. For any point $y$ in the source of $f$, the neighborhood filter of $(f.\text{extend}\, I)(y)$ within the target of the extended chart $f.\text{extend}\, I$ is equal to the neighborhood filter of $(f.\text{extend}\, I)(y)$ within the range of $I$. In other words: $$\mathcal{N}_{(f.\text{extend}\, I).\text{target}}((f.\text{extend}\, I)(y)) = \mathcal{N}_{\text{range}(I)}((f.\text{extend}\, I)(y)).$$

PartialHomeomorph.extend_target_eventuallyEq theorem

{y : M} (hy : y ∈ f.source) : (f.extend I).target =ᶠ[𝓝 (f.extend I y)] range I

Full source

theorem extend_target_eventuallyEq {y : M} (hy : y ∈ f.source) :
    (f.extend I).target =ᶠ[𝓝 (f.extend I y)] range I :=
  nhdsWithin_eq_iff_eventuallyEq.1 (nhdsWithin_extend_target_eq _ hy)

Eventual Equality of Extended Chart Target and Model Range

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$ with model embedding $I : H \to E$, and let $f$ be a chart on $M$. For any point $y$ in the source of $f$, the target of the extended chart $f.\text{extend}\, I$ is eventually equal to the range of $I$ in the neighborhood filter of $(f.\text{extend}\, I)(y)$. In other words: $$(f.\text{extend}\, I).\text{target} =_{\mathcal{N}((f.\text{extend}\, I)(y))} \text{range}(I).$$

PartialHomeomorph.continuousAt_extend_symm' theorem

{x : E} (h : x ∈ (f.extend I).target) : ContinuousAt (f.extend I).symm x

Full source

theorem continuousAt_extend_symm' {x : E} (h : x ∈ (f.extend I).target) :
    ContinuousAt (f.extend I).symm x :=
  (f.continuousAt_symm h.2).comp I.continuous_symm.continuousAt

Continuity of the Inverse Extended Chart at Points in Its Target

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$, and let $f$ be a partial homeomorphism (chart) on $M$. For any point $x$ in the target of the extended chart $f.\text{extend}\, I$ (which is a partial equivalence from $M$ to $E$), the inverse map $(f.\text{extend}\, I)^{-1}$ is continuous at $x$.

PartialHomeomorph.continuousAt_extend_symm theorem

{x : M} (h : x ∈ f.source) : ContinuousAt (f.extend I).symm (f.extend I x)

Full source

theorem continuousAt_extend_symm {x : M} (h : x ∈ f.source) :
    ContinuousAt (f.extend I).symm (f.extend I x) :=
  continuousAt_extend_symm' f <| (f.extend I).map_source <| by rwa [f.extend_source]

Continuity of Inverse Extended Chart at Image Points

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$ via the model with corners $I$, and let $f$ be a chart on $M$. For any point $x$ in the source of $f$, the inverse of the extended chart $(f.\text{extend}\, I)^{-1}$ is continuous at the image point $(f.\text{extend}\, I)(x) \in E$.

PartialHomeomorph.continuousOn_extend_symm theorem

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

Full source

theorem continuousOn_extend_symm : ContinuousOn (f.extend I).symm (f.extend I).target := fun _ h =>
  (continuousAt_extend_symm' _ h).continuousWithinAt

Continuity of the Inverse Extended Chart on Its Target

Informal description

For any partial homeomorphism $f$ on a manifold with corners modeled on $(E, H)$, the inverse of the extended chart $(f.\text{extend}\, I)^{-1}$ is continuous on its target set, which is the image of $f.\text{extend}\, I$ in $E$.

PartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff theorem

 {X} [TopologicalSpace X] {g : M → X} {s : Set M} {x : M} :
  ContinuousWithinAt (g ∘ (f.extend I).symm) ((f.extend I).symm ⁻¹' s ∩ range I) (f.extend I x) ↔
    ContinuousWithinAt (g ∘ f.symm) (f.symm ⁻¹' s) (f x)

Full source

theorem extend_symm_continuousWithinAt_comp_right_iff {X} [TopologicalSpace X] {g : M → X}
    {s : Set M} {x : M} :
    ContinuousWithinAtContinuousWithinAt (g ∘ (f.extend I).symm) ((f.extend I).symm ⁻¹' s ∩ range I) (f.extend I x) ↔
      ContinuousWithinAt (g ∘ f.symm) (f.symm ⁻¹' s) (f x) := by
  rw [← I.symm_continuousWithinAt_comp_right_iff]; rfl

Equivalence of Continuity for Composition with Extended Chart Inverse

Informal description

Let $M$ be a smooth manifold with corners modeled on $(E, H)$ via the model with corners $I$, and let $f$ be a chart on $M$. For any topological space $X$, function $g \colon M \to X$, subset $s \subseteq M$, and point $x \in M$, the composition $g \circ (f.\text{extend}\, I)^{-1}$ is continuous within $(f.\text{extend}\, I)^{-1}(s) \cap \text{range}(I)$ at $(f.\text{extend}\, I)(x)$ if and only if the composition $g \circ f^{-1}$ is continuous within $f^{-1}(s)$ at $f(x)$.

PartialHomeomorph.isOpen_extend_preimage' theorem

{s : Set E} (hs : IsOpen s) : IsOpen ((f.extend I).source ∩ f.extend I ⁻¹' s)

Full source

theorem isOpen_extend_preimage' {s : Set E} (hs : IsOpen s) :
    IsOpen ((f.extend I).source ∩ f.extend I ⁻¹' s) :=
  (continuousOn_extend f).isOpen_inter_preimage (isOpen_extend_source _) hs

Openness of Preimage under Extended Chart

Informal description

Let $M$ be a smooth manifold with corners modeled on $(E, H)$ via the model with corners $I$, and let $f$ be a chart on $M$. For any open subset $s \subseteq E$, the intersection of the source of the extended chart $f.\text{extend}\, I$ with the preimage of $s$ under $f.\text{extend}\, I$ is an open subset of $M$. In other words, if $s$ is open in $E$, then $(f.\text{extend}\, I)^{-1}(s) \cap \text{dom}(f.\text{extend}\, I)$ is open in $M$.

PartialHomeomorph.isOpen_extend_preimage theorem

{s : Set E} (hs : IsOpen s) : IsOpen (f.source ∩ f.extend I ⁻¹' s)

Full source

theorem isOpen_extend_preimage {s : Set E} (hs : IsOpen s) :
    IsOpen (f.source ∩ f.extend I ⁻¹' s) := by
  rw [← extend_source f (I := I)]; exact isOpen_extend_preimage' f hs

Openness of Preimage under Extended Chart Restricted to Source

Informal description

Let $M$ be a smooth manifold with corners modeled on $(E, H)$ via the model with corners $I$, and let $f$ be a chart on $M$. For any open subset $s \subseteq E$, the intersection of the source of $f$ with the preimage of $s$ under the extended chart $f.\text{extend}\, I$ is an open subset of $M$. In other words, if $s$ is open in $E$, then $f^{-1}(s) \cap \text{dom}(f)$ is open in $M$.

PartialHomeomorph.map_extend_nhdsWithin_eq_image theorem

 {y : M} (hy : y ∈ f.source) : map (f.extend I) (𝓝[s] y) = 𝓝[f.extend I '' ((f.extend I).source ∩ s)] f.extend I y

Full source

theorem map_extend_nhdsWithin_eq_image {y : M} (hy : y ∈ f.source) :
    map (f.extend I) (𝓝[s] y) = 𝓝[f.extend I '' ((f.extend I).source ∩ s)] f.extend I y := by
  set e := f.extend I
  calc
    map e (𝓝[s] y) = map e (𝓝[e.source ∩ s] y) :=
      congr_arg (map e) (nhdsWithin_inter_of_mem (extend_source_mem_nhdsWithin f hy)).symm
    _ = 𝓝[e '' (e.source ∩ s)] e y :=
      ((f.extend I).leftInvOn.mono inter_subset_left).map_nhdsWithin_eq
        ((f.extend I).left_inv <| by rwa [f.extend_source])
        (continuousAt_extend_symm f hy).continuousWithinAt
        (continuousAt_extend f hy).continuousWithinAt

Equality of Neighborhood Filters under Extended Chart Mapping

Informal description

Let $M$ be a smooth manifold with corners modeled on $(E, H)$ via the model with corners $I$, and let $f$ be a chart on $M$. For any point $y$ in the source of $f$ and any subset $s \subseteq M$, the image under the extended chart $f.\text{extend}\, I$ of the neighborhood filter of $y$ within $s$ equals the neighborhood filter of $f.\text{extend}\, I(y)$ within the image of the intersection of the source of $f.\text{extend}\, I$ with $s$. In other words, for $y \in f.\text{source}$, we have: $$(f.\text{extend}\, I)_*(\mathcal{N}_s(y)) = \mathcal{N}_{(f.\text{extend}\, I)(\text{source}(f.\text{extend}\, I) \cap s)}(f.\text{extend}\, I(y))$$

PartialHomeomorph.map_extend_nhdsWithin_eq_image_of_subset theorem

{y : M} (hy : y ∈ f.source) (hs : s ⊆ f.source) : map (f.extend I) (𝓝[s] y) = 𝓝[f.extend I '' s] f.extend I y

Full source

theorem map_extend_nhdsWithin_eq_image_of_subset {y : M} (hy : y ∈ f.source) (hs : s ⊆ f.source) :
    map (f.extend I) (𝓝[s] y) = 𝓝[f.extend I '' s] f.extend I y := by
  rw [map_extend_nhdsWithin_eq_image _ hy, inter_eq_self_of_subset_right]
  rwa [extend_source]

Equality of Neighborhood Filters under Extended Chart Mapping for Subsets of Chart Domain

Informal description

Let $M$ be a smooth manifold with corners modeled on $(E, H)$ via the model with corners $I$, and let $f$ be a chart on $M$. For any point $y$ in the source of $f$ and any subset $s \subseteq f.\text{source}$, the image under the extended chart $f.\text{extend}\, I$ of the neighborhood filter of $y$ within $s$ equals the neighborhood filter of $f.\text{extend}\, I(y)$ within the image of $s$ under $f.\text{extend}\, I$. In other words, for $y \in f.\text{source}$ and $s \subseteq f.\text{source}$, we have: $$(f.\text{extend}\, I)_*(\mathcal{N}_s(y)) = \mathcal{N}_{(f.\text{extend}\, I)(s)}(f.\text{extend}\, I(y))$$

PartialHomeomorph.map_extend_nhdsWithin theorem

 {y : M} (hy : y ∈ f.source) : map (f.extend I) (𝓝[s] y) = 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I y

Full source

theorem map_extend_nhdsWithin {y : M} (hy : y ∈ f.source) :
    map (f.extend I) (𝓝[s] y) = 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I y := by
  rw [map_extend_nhdsWithin_eq_image f hy, nhdsWithin_inter, ←
    nhdsWithin_extend_target_eq _ hy, ← nhdsWithin_inter, (f.extend I).image_source_inter_eq',
    inter_comm]

Equality of Neighborhood Filters under Extended Chart Mapping with Preimage Condition

Informal description

Let $M$ be a smooth manifold with corners modeled on $(E, H)$ via the model with corners $I$, and let $f$ be a chart on $M$. For any point $y$ in the source of $f$ and any subset $s \subseteq M$, the image under the extended chart $f.\text{extend}\, I$ of the neighborhood filter of $y$ within $s$ equals the neighborhood filter of $f.\text{extend}\, I(y)$ within the intersection of the preimage of $s$ under the inverse of $f.\text{extend}\, I$ and the range of $I$. In other words, for $y \in f.\text{source}$, we have: $$(f.\text{extend}\, I)_*(\mathcal{N}_s(y)) = \mathcal{N}_{(f.\text{extend}\, I)^{-1}(s) \cap \text{range}(I)}(f.\text{extend}\, I(y))$$

PartialHomeomorph.map_extend_symm_nhdsWithin theorem

 {y : M} (hy : y ∈ f.source) : map (f.extend I).symm (𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I y) = 𝓝[s] y

Full source

theorem map_extend_symm_nhdsWithin {y : M} (hy : y ∈ f.source) :
    map (f.extend I).symm (𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I y) = 𝓝[s] y := by
  rw [← map_extend_nhdsWithin f hy, map_map, Filter.map_congr, map_id]
  exact (f.extend I).leftInvOn.eqOn.eventuallyEq_of_mem (extend_source_mem_nhdsWithin _ hy)

Inverse Extended Chart Preserves Neighborhood Filters with Preimage Condition

Informal description

Let $M$ be a smooth manifold with corners modeled on $(E, H)$ via the model with corners $I$, and let $f$ be a chart on $M$. For any point $y$ in the source of $f$ and any subset $s \subseteq M$, the image under the inverse of the extended chart $(f.\text{extend}\, I)^{-1}$ of the neighborhood filter of $f.\text{extend}\, I(y)$ within $(f.\text{extend}\, I)^{-1}(s) \cap \text{range}(I)$ equals the neighborhood filter of $y$ within $s$. In other words, for $y \in f.\text{source}$, we have: $$(f.\text{extend}\, I)^{-1}_*(\mathcal{N}_{(f.\text{extend}\, I)^{-1}(s) \cap \text{range}(I)}(f.\text{extend}\, I(y))) = \mathcal{N}_s(y)$$

PartialHomeomorph.map_extend_symm_nhdsWithin_range theorem

{y : M} (hy : y ∈ f.source) : map (f.extend I).symm (𝓝[range I] f.extend I y) = 𝓝 y

Full source

theorem map_extend_symm_nhdsWithin_range {y : M} (hy : y ∈ f.source) :
    map (f.extend I).symm (𝓝[range I] f.extend I y) = 𝓝 y := by
  rw [← nhdsWithin_univ, ← map_extend_symm_nhdsWithin f (I := I) hy, preimage_univ, univ_inter]

Inverse Extended Chart Preserves Neighborhood Filters within Range

Informal description

Let $M$ be a smooth manifold with corners modeled on $(E, H)$ via the model with corners $I$, and let $f$ be a chart on $M$. For any point $y$ in the source of $f$, the image under the inverse of the extended chart $(f.\text{extend}\, I)^{-1}$ of the neighborhood filter of $f.\text{extend}\, I(y)$ within the range of $I$ equals the neighborhood filter of $y$. In other words, for $y \in f.\text{source}$, we have: $$(f.\text{extend}\, I)^{-1}_*(\mathcal{N}_{\text{range}(I)}(f.\text{extend}\, I(y))) = \mathcal{N}(y)$$

PartialHomeomorph.tendsto_extend_comp_iff theorem

 {α : Type*} {l : Filter α} {g : α → M} (hg : ∀ᶠ z in l, g z ∈ f.source) {y : M} (hy : y ∈ f.source) :
  Tendsto (f.extend I ∘ g) l (𝓝 (f.extend I y)) ↔ Tendsto g l (𝓝 y)

Full source

theorem tendsto_extend_comp_iff {α : Type*} {l : Filter α} {g : α → M}
    (hg : ∀ᶠ z in l, g z ∈ f.source) {y : M} (hy : y ∈ f.source) :
    TendstoTendsto (f.extend I ∘ g) l (𝓝 (f.extend I y)) ↔ Tendsto g l (𝓝 y) := by
  refine ⟨fun h u hu ↦ mem_map.2 ?_, (continuousAt_extend _ hy).tendsto.comp⟩
  have := (f.continuousAt_extend_symm hy).tendsto.comp h
  rw [extend_left_inv _ hy] at this
  filter_upwards [hg, mem_map.1 (this hu)] with z hz hzu
  simpa only [(· ∘ ·), extend_left_inv _ hz, mem_preimage] using hzu

Limit Equivalence for Extended Chart Compositions

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$ via the model with corners $I$, and let $f$ be a chart on $M$. For any filter $l$ on a type $\alpha$, any function $g \colon \alpha \to M$ such that $g(z)$ is eventually in the source of $f$ for $z$ in $l$, and any point $y$ in the source of $f$, the following equivalence holds: The composition $f.\text{extend}\, I \circ g$ tends to $f.\text{extend}\, I(y)$ along $l$ if and only if $g$ tends to $y$ along $l$.

PartialHomeomorph.continuousWithinAt_writtenInExtend_iff theorem

 {f' : PartialHomeomorph M' H'} {g : M → M'} {y : M} (hy : y ∈ f.source) (hgy : g y ∈ f'.source)
  (hmaps : MapsTo g s f'.source) :
  ContinuousWithinAt (f'.extend I' ∘ g ∘ (f.extend I).symm) ((f.extend I).symm ⁻¹' s ∩ range I) (f.extend I y) ↔
    ContinuousWithinAt g s y

Full source

theorem continuousWithinAt_writtenInExtend_iff {f' : PartialHomeomorph M' H'} {g : M → M'} {y : M}
    (hy : y ∈ f.source) (hgy : g y ∈ f'.source) (hmaps : MapsTo g s f'.source) :
    ContinuousWithinAtContinuousWithinAt (f'.extend I' ∘ g ∘ (f.extend I).symm)
      ((f.extend I).symm ⁻¹' s ∩ range I) (f.extend I y) ↔ ContinuousWithinAt g s y := by
  unfold ContinuousWithinAt
  simp only [comp_apply]
  rw [extend_left_inv _ hy, f'.tendsto_extend_comp_iff _ hgy,
    ← f.map_extend_symm_nhdsWithin (I := I) hy, tendsto_map'_iff]
  rw [← f.map_extend_nhdsWithin (I := I) hy, eventually_map]
  filter_upwards [inter_mem_nhdsWithin _ (f.open_source.mem_nhds hy)] with z hz
  rw [comp_apply, extend_left_inv _ hz.2]
  exact hmaps hz.1

Equivalence of Continuity Conditions for Manifold Maps via Extended Charts

Informal description

Let $M$ and $M'$ be manifolds with corners modeled on $(E,H)$ and $(E',H')$ via models with corners $I$ and $I'$ respectively. Let $f$ and $f'$ be charts on $M$ and $M'$ respectively, and let $g : M \to M'$ be a map between the manifolds. For a point $y \in f.\text{source}$ such that $g(y) \in f'.\text{source}$, and assuming $g$ maps $s$ into $f'.\text{source}$, the following equivalence holds: The composition $f'.\text{extend}\, I' \circ g \circ (f.\text{extend}\, I)^{-1}$ is continuous at $(f.\text{extend}\, I)(y)$ within $(f.\text{extend}\, I)^{-1}(s) \cap \text{range}(I)$ if and only if $g$ is continuous at $y$ within $s$.

PartialHomeomorph.continuousOn_writtenInExtend_iff theorem

 {f' : PartialHomeomorph M' H'} {g : M → M'} (hs : s ⊆ f.source) (hmaps : MapsTo g s f'.source) :
  ContinuousOn (f'.extend I' ∘ g ∘ (f.extend I).symm) (f.extend I '' s) ↔ ContinuousOn g s

Full source

/-- 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 continuousOn_writtenInExtend_iff {f' : PartialHomeomorph M' H'} {g : M → M'}
    (hs : s ⊆ f.source) (hmaps : MapsTo g s f'.source) :
    ContinuousOnContinuousOn (f'.extend I' ∘ g ∘ (f.extend I).symm) (f.extend I '' s) ↔ ContinuousOn g s := by
  refine forall_mem_image.trans <| forall₂_congr fun x hx ↦ ?_
  refine (continuousWithinAt_congr_set ?_).trans
    (continuousWithinAt_writtenInExtend_iff _ (hs hx) (hmaps hx) hmaps)
  rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin_eq_image_of_subset,
    ← map_extend_nhdsWithin]
  exacts [hs hx, hs hx, hs]

Equivalence of Continuity for Manifold Maps via Extended Charts on Subsets

Informal description

Let $M$ and $M'$ be smooth manifolds with corners modeled on $(E,H)$ and $(E',H')$ via models with corners $I$ and $I'$ respectively. Let $f$ and $f'$ be charts on $M$ and $M'$, and let $g : M \to M'$ be a map between the manifolds. For a subset $s \subseteq f.\text{source}$ such that $g$ maps $s$ into $f'.\text{source}$, the following equivalence holds: The composition $f'.\text{extend}\, I' \circ g \circ (f.\text{extend}\, I)^{-1}$ is continuous on the image $f.\text{extend}\, I(s)$ if and only if $g$ is continuous on $s$.

PartialHomeomorph.extend_preimage_mem_nhdsWithin theorem

 {x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝[s] x) :
  (f.extend I).symm ⁻¹' t ∈ 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I x

Full source

/-- 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 extend_preimage_mem_nhdsWithin {x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝[s] x) :
    (f.extend I).symm ⁻¹' t(f.extend I).symm ⁻¹' t ∈ 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I x := by
  rwa [← map_extend_symm_nhdsWithin f (I := I) h, mem_map] at ht

Neighborhood Preservation under Extended Chart Inverse within a Set

Informal description

Let $M$ be a smooth manifold with corners modeled on $(E, H)$ via the model with corners $I$, and let $f$ be a chart on $M$. For any point $x$ in the source of $f$ and any neighborhood $t$ of $x$ within a subset $s \subseteq M$, the preimage of $t$ under the inverse of the extended chart $(f \circ I)^{-1}$ is a neighborhood of $(f \circ I)(x)$ within $(f \circ I)^{-1}(s) \cap \text{range}(I)$. In other words, for $x \in f.\text{source}$ and $t \in \mathcal{N}_s(x)$, we have: $$(f \circ I)^{-1}(t) \in \mathcal{N}_{(f \circ I)^{-1}(s) \cap \text{range}(I)}((f \circ I)(x))$$

PartialHomeomorph.extend_preimage_mem_nhds theorem

{x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝 x) : (f.extend I).symm ⁻¹' t ∈ 𝓝 (f.extend I x)

Full source

theorem extend_preimage_mem_nhds {x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝 x) :
    (f.extend I).symm ⁻¹' t(f.extend I).symm ⁻¹' t ∈ 𝓝 (f.extend I x) := by
  apply (continuousAt_extend_symm f h).preimage_mem_nhds
  rwa [(f.extend I).left_inv]
  rwa [f.extend_source]

Neighborhood Preservation under Extended Chart Inverse

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$, and let $f$ be a partial homeomorphism on $M$ with model embedding $I : H \to E$. For any point $x \in f.\text{source}$ and any neighborhood $t$ of $x$ in $M$, the preimage of $t$ under the inverse of the extended chart $(f.\text{extend}\, I)^{-1}$ is a neighborhood of $f.\text{extend}\, I(x)$ in $E$.

PartialHomeomorph.extend_preimage_inter_eq theorem

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

Full source

/-- 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 extend_preimage_inter_eq :
    (f.extend I).symm ⁻¹' (s ∩ t)(f.extend I).symm ⁻¹' (s ∩ t) ∩ range I =
      (f.extend I).symm ⁻¹' s(f.extend I).symm ⁻¹' s ∩ range I(f.extend I).symm ⁻¹' s ∩ range I ∩ (f.extend I).symm ⁻¹' t := by
  mfld_set_tac

Preimage of Intersection under Extended Chart Inverse

Informal description

Let $f$ be a partial homeomorphism on a manifold $M$ modeled on $(E, H)$, and let $I$ be a model with corners embedding $H$ into $E$. For any sets $s, t \subseteq M$, the preimage under the extended chart's inverse map satisfies: \[ (f.\text{extend}\, I)^{-1}(s \cap t) \cap \text{range}\, I = (f.\text{extend}\, I)^{-1}(s) \cap \text{range}\, I \cap (f.\text{extend}\, I)^{-1}(t). \]

PartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq_aux theorem

 {s : Set M} {x : M} (hx : x ∈ f.source) :
  ((f.extend I).symm ⁻¹' s ∩ range I : Set _) =ᶠ[𝓝 (f.extend I x)]
    ((f.extend I).target ∩ (f.extend I).symm ⁻¹' s : Set _)

Full source

theorem extend_symm_preimage_inter_range_eventuallyEq_aux {s : Set M} {x : M} (hx : x ∈ f.source) :
    ((f.extend I).symm ⁻¹' s ∩ range I : Set _) =ᶠ[𝓝 (f.extend I x)]
      ((f.extend I).target ∩ (f.extend I).symm ⁻¹' s : Set _) := by
  rw [f.extend_target, inter_assoc, inter_comm (range I)]
  conv =>
    congr
    · skip
    rw [← univ_inter (_ ∩ range I)]
  refine (eventuallyEq_univ.mpr ?_).symm.inter EventuallyEq.rfl
  refine I.continuousAt_symm.preimage_mem_nhds (f.open_target.mem_nhds ?_)
  simp_rw [f.extend_coe, Function.comp_apply, I.left_inv, f.mapsTo hx]

Local Equality of Extended Chart Preimage and Target Intersection in Neighborhood Filter

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$, and let $f$ be a partial homeomorphism on $M$ with model embedding $I : H \to E$. For any set $s \subseteq M$ and any point $x \in f.\text{source}$, the following equality holds in the neighborhood filter of $f.\text{extend}\, I(x)$: \[ (f.\text{extend}\, I)^{-1}(s) \cap \text{range}\, I =_{\mathcal{N}(f.\text{extend}\, I(x))} (f.\text{extend}\, I).\text{target} \cap (f.\text{extend}\, I)^{-1}(s). \] Here, $=_{\mathcal{N}(a)}$ denotes equality in the neighborhood filter of $a$.

PartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq theorem

 {s : Set M} {x : M} (hs : s ⊆ f.source) (hx : x ∈ f.source) :
  ((f.extend I).symm ⁻¹' s ∩ range I : Set _) =ᶠ[𝓝 (f.extend I x)] f.extend I '' s

Full source

theorem extend_symm_preimage_inter_range_eventuallyEq {s : Set M} {x : M} (hs : s ⊆ f.source)
    (hx : x ∈ f.source) :
    ((f.extend I).symm ⁻¹' s ∩ range I : Set _) =ᶠ[𝓝 (f.extend I x)] f.extend I '' s := by
  rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin _ hx,
    map_extend_nhdsWithin_eq_image_of_subset _ hx hs]

Local Equality of Extended Chart Preimage and Image in Neighborhood Filter

Informal description

Let $M$ be a smooth manifold with corners modeled on $(E, H)$ via the model with corners $I : H \to E$, and let $f$ be a chart on $M$. For any subset $s \subseteq f.\text{source}$ and any point $x \in f.\text{source}$, the intersection of the preimage of $s$ under the inverse of the extended chart $f.\text{extend}\, I$ with the range of $I$ is eventually equal to the image of $s$ under $f.\text{extend}\, I$ in the neighborhood filter of $f.\text{extend}\, I(x)$. In other words, for $s \subseteq f.\text{source}$ and $x \in f.\text{source}$, we have: $$(f.\text{extend}\, I)^{-1}(s) \cap \text{range}\, I =_{\mathcal{N}(f.\text{extend}\, I(x))} (f.\text{extend}\, I)(s)$$

PartialHomeomorph.extend_coord_change_source theorem

: ((f.extend I).symm ≫ f'.extend I).source = I '' (f.symm ≫ₕ f').source

Full source

theorem extend_coord_change_source :
    ((f.extend I).symm ≫ f'.extend I).source = I '' (f.symm ≫ₕ f').source := by
  simp_rw [PartialEquiv.trans_source, I.image_eq, extend_source, PartialEquiv.symm_source,
    extend_target, inter_right_comm _ (range I)]
  rfl

Source of Extended Coordinate Change Equals Image of Original Coordinate Change Source

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$, and let $I : H \to E$ be the model embedding. For any two charts $f$ and $f'$ in the maximal atlas of $M$, the source of the extended coordinate change $(f.\text{extend}\, I)^{-1} \circ f'.\text{extend}\, I$ equals the image under $I$ of the source of the coordinate change $f^{-1} \circ f'$ between the original charts. In symbols: $$\text{source}\left((f.\text{extend}\, I)^{-1} \circ f'.\text{extend}\, I\right) = I\left(\text{source}(f^{-1} \circ f')\right)$$

PartialHomeomorph.extend_image_source_inter theorem

: f.extend I '' (f.source ∩ f'.source) = ((f.extend I).symm ≫ f'.extend I).source

Full source

theorem extend_image_source_inter :
    f.extend I '' (f.source ∩ f'.source) = ((f.extend I).symm ≫ f'.extend I).source := by
  simp_rw [f.extend_coord_change_source, f.extend_coe, image_comp I f, trans_source'', symm_symm,
    symm_target]

Image of Source Intersection under Extended Chart Equals Source of Extended Coordinate Change

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$, and let $I : H \to E$ be the model embedding. For any two charts $f$ and $f'$ in the maximal atlas of $M$, the image under the extended chart $f.\text{extend}\, I$ of the intersection of their source sets equals the source of the extended coordinate change $(f.\text{extend}\, I)^{-1} \circ f'.\text{extend}\, I$. In symbols: $$(f.\text{extend}\, I)(f.\text{source} \cap f'.\text{source}) = \text{source}\left((f.\text{extend}\, I)^{-1} \circ f'.\text{extend}\, I\right)$$

PartialHomeomorph.extend_coord_change_source_mem_nhdsWithin theorem

 {x : E} (hx : x ∈ ((f.extend I).symm ≫ f'.extend I).source) : ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] x

Full source

theorem extend_coord_change_source_mem_nhdsWithin {x : E}
    (hx : x ∈ ((f.extend I).symm ≫ f'.extend I).source) :
    ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] x := by
  rw [f.extend_coord_change_source] at hx ⊢
  obtain ⟨x, hx, rfl⟩ := hx
  refine I.image_mem_nhdsWithin ?_
  exact (PartialHomeomorph.open_source _).mem_nhds hx

Extended Coordinate Change Source is a Neighborhood within the Model Embedding Range

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$, and let $I : H \to E$ be the model embedding. For any two charts $f$ and $f'$ in the maximal atlas of $M$, if $x$ belongs to the source of the extended coordinate change $(f.\text{extend}\, I)^{-1} \circ f'.\text{extend}\, I$, then this source is a neighborhood of $x$ within the range of $I$ in $E$. In symbols, for any $x \in E$ such that $x \in \text{source}\left((f.\text{extend}\, I)^{-1} \circ f'.\text{extend}\, I\right)$, we have: $$\text{source}\left((f.\text{extend}\, I)^{-1} \circ f'.\text{extend}\, I\right) \in \mathcal{N}_{\text{range}(I)}(x)$$

PartialHomeomorph.extend_coord_change_source_mem_nhdsWithin' theorem

 {x : M} (hxf : x ∈ f.source) (hxf' : x ∈ f'.source) :
  ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] f.extend I x

Full source

theorem extend_coord_change_source_mem_nhdsWithin' {x : M} (hxf : x ∈ f.source)
    (hxf' : x ∈ f'.source) :
    ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] f.extend I x := by
  apply extend_coord_change_source_mem_nhdsWithin
  rw [← extend_image_source_inter]
  exact mem_image_of_mem _ ⟨hxf, hxf'⟩

Neighborhood Property of Extended Coordinate Change Source for Points in Chart Domains

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$, and let $I : H \to E$ be the model embedding. For any two charts $f$ and $f'$ in the maximal atlas of $M$ and any point $x \in M$ that lies in both $f.\text{source}$ and $f'.\text{source}$, the source of the extended coordinate change $(f.\text{extend}\, I)^{-1} \circ f'.\text{extend}\, I$ is a neighborhood of $f.\text{extend}\, I(x)$ within the range of $I$ in $E$. In symbols, for any $x \in M$ with $x \in f.\text{source}$ and $x \in f'.\text{source}$, we have: $$\text{source}\left((f.\text{extend}\, I)^{-1} \circ f'.\text{extend}\, I\right) \in \mathcal{N}_{\text{range}(I)}(f.\text{extend}\, I(x))$$

PartialHomeomorph.contDiffOn_extend_coord_change theorem

 [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M) (hf' : f' ∈ maximalAtlas I n M) :
  ContDiffOn 𝕜 n (f.extend I ∘ (f'.extend I).symm) ((f'.extend I).symm ≫ f.extend I).source

Full source

theorem contDiffOn_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
    (hf' : f' ∈ maximalAtlas I n M) :
    ContDiffOn 𝕜 n (f.extend I ∘ (f'.extend I).symm) ((f'.extend I).symm ≫ f.extend I).source := by
  rw [extend_coord_change_source, I.image_eq]
  exact (StructureGroupoid.compatible_of_mem_maximalAtlas hf' hf).1

$C^n$ Differentiability of Extended Coordinate Changes on Manifolds with Corners

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$, and let $I : H \to E$ be the model embedding. For any two charts $f$ and $f'$ in the maximal atlas of $M$, the composition $f \circ I^{-1} \circ I \circ f'^{-1}$ is $C^n$ on its domain of definition. More precisely, the map $f \circ I^{-1} \circ I \circ f'^{-1}$ is $C^n$ on the set $(f' \circ I^{-1} \circ I \circ f^{-1})^{-1}(\text{domain of } f \circ I^{-1} \circ I \circ f'^{-1})$.

PartialHomeomorph.contDiffWithinAt_extend_coord_change theorem

 [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M) (hf' : f' ∈ maximalAtlas I n M) {x : E}
  (hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source) :
  ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) x

Full source

theorem contDiffWithinAt_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
    (hf' : f' ∈ maximalAtlas I n M) {x : E} (hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source) :
    ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) x := by
  apply (contDiffOn_extend_coord_change hf hf' x hx).mono_of_mem_nhdsWithin
  rw [extend_coord_change_source] at hx ⊢
  obtain ⟨z, hz, rfl⟩ := hx
  exact I.image_mem_nhdsWithin ((PartialHomeomorph.open_source _).mem_nhds hz)

$C^n$ Differentiability of Extended Coordinate Changes at a Point in Manifolds with Corners

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$, and let $I : H \to E$ be the model embedding. For any two charts $f$ and $f'$ in the maximal atlas of $M$, and any point $x \in E$ in the domain of the extended coordinate change $(f'.\text{extend}\, I)^{-1} \circ f.\text{extend}\, I$, the composition $f \circ I^{-1} \circ I \circ f'^{-1}$ is $C^n$ at $x$ within the range of $I$.

PartialHomeomorph.contDiffWithinAt_extend_coord_change' theorem

 [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M) (hf' : f' ∈ maximalAtlas I n M) {x : M} (hxf : x ∈ f.source)
  (hxf' : x ∈ f'.source) : ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) (f'.extend I x)

Full source

theorem contDiffWithinAt_extend_coord_change' [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
    (hf' : f' ∈ maximalAtlas I n M) {x : M} (hxf : x ∈ f.source) (hxf' : x ∈ f'.source) :
    ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) (f'.extend I x) := by
  refine contDiffWithinAt_extend_coord_change hf hf' ?_
  rw [← extend_image_source_inter]
  exact mem_image_of_mem _ ⟨hxf', hxf⟩

$C^n$ Differentiability of Extended Coordinate Changes at a Point in Manifolds with Corners (Point Version)

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$, and let $I : H \to E$ be the model embedding. For any two charts $f$ and $f'$ in the maximal atlas of $M$, and any point $x \in M$ that lies in both the source of $f$ and $f'$, the composition $f \circ I^{-1} \circ I \circ f'^{-1}$ is $C^n$ at the point $f'(x) \in E$ within the range of $I$.

extChartAt definition

(x : M) : PartialEquiv M E

Full source

/-- The preferred extended chart on a manifold with corners around a point `x`, from a neighborhood
of `x` to the model vector space. -/
@[simp, mfld_simps]
def extChartAt (x : M) : PartialEquiv M E :=
  (chartAt H x).extend I

Extended chart at a point in a manifold with corners

Informal description

The extended chart at a point $ x $ in a manifold $ M $ modeled on $ (E, H) $ is a partial equivalence between $ M $ and the model vector space $ E $, obtained by composing the chart at $ x $ with the model embedding $ I : H \to E $. More precisely, for $ x \in M $, the extended chart $ \text{extChartAt}_I(x) $ is defined as the composition of the chart $ \text{chartAt}_H(x) $ (a local homeomorphism from a neighborhood of $ x $ in $ M $ to $ H $) with the model embedding $ I $. This yields a partial equivalence whose source is the domain of $ \text{chartAt}_H(x) $ and whose target is the image of $ I \circ \text{chartAt}_H(x) $ in $ E $. The inverse of this partial equivalence is given by $ \text{chartAt}_H(x)^{-1} \circ I^{-1} $.

extChartAt_coe theorem

(x : M) : ⇑(extChartAt I x) = I ∘ chartAt H x

Full source

theorem extChartAt_coe (x : M) : ⇑(extChartAt I x) = I ∘ chartAt H x :=
  rfl

Extended Chart as Composition of Model Embedding and Chart

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the extended chart map $\text{extChartAt}_I(x)$ is equal to the composition of the model embedding $I : H \to E$ with the chart map $\text{chartAt}_H(x)$ at $x$.

extChartAt_coe_symm theorem

(x : M) : ⇑(extChartAt I x).symm = (chartAt H x).symm ∘ I.symm

Full source

theorem extChartAt_coe_symm (x : M) : ⇑(extChartAt I x).symm = (chartAt H x).symm ∘ I.symm :=
  rfl

Inverse of Extended Chart as Composition of Inverses

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the inverse of the extended chart $\text{extChartAt}_I(x)^{-1}$ is equal to the composition of the inverse of the model embedding $I^{-1}$ with the inverse of the chart $\text{chartAt}_H(x)^{-1}$. In other words, the inverse function of the extended chart at $x$ is given by: $$ \text{extChartAt}_I(x)^{-1} = \text{chartAt}_H(x)^{-1} \circ I^{-1} $$

extChartAt_source theorem

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

Full source

theorem extChartAt_source (x : M) : (extChartAt I x).source = (chartAt H x).source :=
  extend_source _

Source Equality for Extended Chart and Original Chart

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the source of the extended chart $\text{extChartAt}_I(x)$ equals the source of the chart $\text{chartAt}_H(x)$. That is, $$(\text{extChartAt}_I(x)).\text{source} = (\text{chartAt}_H(x)).\text{source}.$$

isOpen_extChartAt_source theorem

(x : M) : IsOpen (extChartAt I x).source

Full source

theorem isOpen_extChartAt_source (x : M) : IsOpen (extChartAt I x).source :=
  isOpen_extend_source _

Openness of the Extended Chart's Source Set

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the source of the extended chart $\text{extChartAt}_I(x)$ is an open subset of $M$.

mem_extChartAt_source theorem

(x : M) : x ∈ (extChartAt I x).source

Full source

theorem mem_extChartAt_source (x : M) : x ∈ (extChartAt I x).source := by
  simp only [extChartAt_source, mem_chart_source]

Point Belongs to Source of Its Extended Chart

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the point $x$ belongs to the source of its extended chart $\text{extChartAt}_I(x)$. That is, $x \in (\text{extChartAt}_I(x)).\text{source}$.

mem_extChartAt_target theorem

(x : M) : extChartAt I x x ∈ (extChartAt I x).target

Full source

theorem mem_extChartAt_target (x : M) : extChartAtextChartAt I x x ∈ (extChartAt I x).target :=
  (extChartAt I x).map_source <| mem_extChartAt_source _

Image of Point under Extended Chart Belongs to Target

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the image of $x$ under its extended chart $\text{extChartAt}_I(x)$ belongs to the target set of the extended chart, i.e., $\text{extChartAt}_I(x)(x) \in (\text{extChartAt}_I(x)).\text{target}$.

extChartAt_target theorem

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

Full source

theorem extChartAt_target (x : M) :
    (extChartAt I x).target = I.symm ⁻¹' (chartAt H x).targetI.symm ⁻¹' (chartAt H x).target ∩ range I :=
  extend_target _

Target of Extended Chart as Preimage Intersection

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the target of the extended chart $\text{extChartAt}_I(x)$ is equal to the intersection of the preimage of the target of the chart $\text{chartAt}_H(x)$ under the inverse model embedding $I^{-1}$ and the range of $I$. That is: $$(\text{extChartAt}_I(x)).\text{target} = I^{-1}\big((\text{chartAt}_H(x)).\text{target}\big) \cap \text{range}(I)$$

uniqueDiffOn_extChartAt_target theorem

(x : M) : UniqueDiffOn 𝕜 (extChartAt I x).target

Full source

theorem uniqueDiffOn_extChartAt_target (x : M) : UniqueDiffOn 𝕜 (extChartAt I x).target := by
  rw [extChartAt_target]
  exact I.uniqueDiffOn_preimage (chartAt H x).open_target

Uniqueness of Derivatives on the Target of Extended Charts

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ with corners over a nontrivially normed field $\mathbb{K}$, the target of the extended chart $\text{extChartAt}_I(x)$ has unique derivatives everywhere. That is, the set $(\text{extChartAt}_I(x)).\text{target} \subseteq E$ satisfies the property that at each of its points, derivatives (if they exist) are uniquely determined.

uniqueDiffWithinAt_extChartAt_target theorem

(x : M) : UniqueDiffWithinAt 𝕜 (extChartAt I x).target (extChartAt I x x)

Full source

theorem uniqueDiffWithinAt_extChartAt_target (x : M) :
    UniqueDiffWithinAt 𝕜 (extChartAt I x).target (extChartAt I x x) :=
  uniqueDiffOn_extChartAt_target x _ <| mem_extChartAt_target x

Uniqueness of Derivatives at the Image Point in Extended Chart Target

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ with corners over a nontrivially normed field $\mathbb{K}$, the target of the extended chart $\text{extChartAt}_I(x)$ has unique derivatives at the point $\text{extChartAt}_I(x)(x)$. That is, the set $(\text{extChartAt}_I(x)).\text{target} \subseteq E$ satisfies the property that derivatives (if they exist) are uniquely determined at $\text{extChartAt}_I(x)(x)$.

extChartAt_to_inv theorem

(x : M) : (extChartAt I x).symm ((extChartAt I x) x) = x

Full source

theorem extChartAt_to_inv (x : M) : (extChartAt I x).symm ((extChartAt I x) x) = x :=
  (extChartAt I x).left_inv (mem_extChartAt_source x)

Inverse Property of Extended Chart at a Point: $(\text{extChartAt}_I(x))^{-1} \circ \text{extChartAt}_I(x)(x) = x$

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ with corners, the composition of the extended chart $\text{extChartAt}_I(x)$ and its inverse maps $x$ back to itself. That is, $(\text{extChartAt}_I(x))^{-1}(\text{extChartAt}_I(x)(x)) = x$.

mapsTo_extChartAt theorem

{x : M} (hs : s ⊆ (chartAt H x).source) : MapsTo (extChartAt I x) s ((extChartAt I x).symm ⁻¹' s ∩ range I)

Full source

theorem mapsTo_extChartAt {x : M} (hs : s ⊆ (chartAt H x).source) :
    MapsTo (extChartAt I x) s ((extChartAt I x).symm ⁻¹' s(extChartAt I x).symm ⁻¹' s ∩ range I) :=
  mapsTo_extend _ hs

Mapping Property of Extended Charts: $\text{extChartAt}_I(x)$ Preserves Preimage-Range Intersection

Informal description

Let $M$ be a manifold modeled on $(E, H)$ with corners, and let $x \in M$. For any subset $s \subseteq M$ contained in the domain of the chart at $x$, the extended chart $\text{extChartAt}_I(x)$ maps $s$ into the intersection of the preimage of $s$ under its inverse and the range of the model embedding $I : H \to E$. In symbols, if $s \subseteq \text{chartAt}_H(x).\text{source}$, then: $$\text{extChartAt}_I(x)(s) \subseteq (\text{extChartAt}_I(x))^{-1}(s) \cap \text{range}(I).$$

extChartAt_source_mem_nhds' theorem

{x x' : M} (h : x' ∈ (extChartAt I x).source) : (extChartAt I x).source ∈ 𝓝 x'

Full source

theorem extChartAt_source_mem_nhds' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
    (extChartAt I x).source ∈ 𝓝 x' :=
  extend_source_mem_nhds _ <| by rwa [← extChartAt_source I]

Neighborhood Property of Extended Chart Source at a Point in Its Domain

Informal description

For any points $x$ and $x'$ in a manifold $M$ modeled on $(E, H)$, if $x'$ belongs to the source of the extended chart $\text{extChartAt}_I(x)$, then the source of $\text{extChartAt}_I(x)$ is a neighborhood of $x'$ in $M$.

extChartAt_source_mem_nhds theorem

(x : M) : (extChartAt I x).source ∈ 𝓝 x

Full source

theorem extChartAt_source_mem_nhds (x : M) : (extChartAt I x).source ∈ 𝓝 x :=
  extChartAt_source_mem_nhds' (mem_extChartAt_source x)

Neighborhood Property of Extended Chart Source at Each Point

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the source of the extended chart $\text{extChartAt}_I(x)$ is a neighborhood of $x$ in $M$.

extChartAt_source_mem_nhdsWithin' theorem

{x x' : M} (h : x' ∈ (extChartAt I x).source) : (extChartAt I x).source ∈ 𝓝[s] x'

Full source

theorem extChartAt_source_mem_nhdsWithin' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
    (extChartAt I x).source ∈ 𝓝[s] x' :=
  mem_nhdsWithin_of_mem_nhds (extChartAt_source_mem_nhds' h)

Neighborhood property of extended chart source within a subset

Informal description

For any points $x$ and $x'$ in a manifold $M$ modeled on $(E, H)$, if $x'$ belongs to the source of the extended chart $\text{extChartAt}_I(x)$, then the source of $\text{extChartAt}_I(x)$ is a neighborhood of $x'$ within any subset $s \subseteq M$.

extChartAt_source_mem_nhdsWithin theorem

(x : M) : (extChartAt I x).source ∈ 𝓝[s] x

Full source

theorem extChartAt_source_mem_nhdsWithin (x : M) : (extChartAt I x).source ∈ 𝓝[s] x :=
  mem_nhdsWithin_of_mem_nhds (extChartAt_source_mem_nhds x)

Neighborhood property of extended chart source within any subset

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ and any subset $s \subseteq M$, the source of the extended chart $\text{extChartAt}_I(x)$ is a neighborhood of $x$ within $s$.

continuousOn_extChartAt theorem

(x : M) : ContinuousOn (extChartAt I x) (extChartAt I x).source

Full source

theorem continuousOn_extChartAt (x : M) : ContinuousOn (extChartAt I x) (extChartAt I x).source :=
  continuousOn_extend _

Continuity of Extended Chart on Its Source Set

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the extended chart $\text{extChartAt}_I(x)$ is continuous on its source set, which consists of all points in $M$ where the chart is defined.

continuousAt_extChartAt' theorem

{x x' : M} (h : x' ∈ (extChartAt I x).source) : ContinuousAt (extChartAt I x) x'

Full source

theorem continuousAt_extChartAt' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
    ContinuousAt (extChartAt I x) x' :=
  continuousAt_extend _ <| by rwa [← extChartAt_source I]

Continuity of Extended Chart at Points in its Source

Informal description

For any points $x$ and $x'$ in a manifold $M$ modeled on $(E, H)$, if $x'$ belongs to the source of the extended chart $\text{extChartAt}_I(x)$, then the extended chart $\text{extChartAt}_I(x)$ is continuous at $x'$. Here, $\text{extChartAt}_I(x)$ denotes the composition of the chart at $x$ with the model embedding $I \colon H \to E$, which maps points from the manifold to the model vector space $E$.

continuousAt_extChartAt theorem

(x : M) : ContinuousAt (extChartAt I x) x

Full source

theorem continuousAt_extChartAt (x : M) : ContinuousAt (extChartAt I x) x :=
  continuousAt_extChartAt' (mem_extChartAt_source x)

Continuity of Extended Chart at Base Point

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the extended chart $\text{extChartAt}_I(x)$ is continuous at $x$. Here, $\text{extChartAt}_I(x)$ denotes the composition of the chart at $x$ with the model embedding $I \colon H \to E$, which maps points from the manifold to the model vector space $E$.

map_extChartAt_nhds' theorem

{x y : M} (hy : y ∈ (extChartAt I x).source) : map (extChartAt I x) (𝓝 y) = 𝓝[range I] extChartAt I x y

Full source

theorem map_extChartAt_nhds' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    map (extChartAt I x) (𝓝 y) = 𝓝[range I] extChartAt I x y :=
  map_extend_nhds _ <| by rwa [← extChartAt_source I]

Neighborhood Filter Preservation under Extended Chart at a Point

Informal description

For any points $x$ and $y$ in a manifold $M$ modeled on $(E, H)$, if $y$ belongs to the source of the extended chart $\text{extChartAt}_I(x)$, then the pushforward of the neighborhood filter $\mathcal{N}(y)$ under $\text{extChartAt}_I(x)$ equals the neighborhood filter of $\text{extChartAt}_I(x)(y)$ restricted to the range of the model embedding $I \colon H \to E$. In other words: $$ (\text{extChartAt}_I(x))_*(\mathcal{N}(y)) = \mathcal{N}_{\text{extChartAt}_I(x)(y)}|_{\text{range}(I)}. $$

map_extChartAt_nhds theorem

(x : M) : map (extChartAt I x) (𝓝 x) = 𝓝[range I] extChartAt I x x

Full source

theorem map_extChartAt_nhds (x : M) : map (extChartAt I x) (𝓝 x) = 𝓝[range I] extChartAt I x x :=
  map_extChartAt_nhds' <| mem_extChartAt_source x

Neighborhood Filter Preservation under Extended Chart at a Point

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the pushforward of the neighborhood filter $\mathcal{N}(x)$ under the extended chart $\text{extChartAt}_I(x)$ equals the neighborhood filter of $\text{extChartAt}_I(x)(x)$ restricted to the range of the model embedding $I \colon H \to E$. In other words: $$ (\text{extChartAt}_I(x))_*(\mathcal{N}(x)) = \mathcal{N}_{\text{extChartAt}_I(x)(x)}|_{\text{range}(I)}. $$

map_extChartAt_nhds_of_boundaryless theorem

[I.Boundaryless] (x : M) : map (extChartAt I x) (𝓝 x) = 𝓝 (extChartAt I x x)

Full source

theorem map_extChartAt_nhds_of_boundaryless [I.Boundaryless] (x : M) :
    map (extChartAt I x) (𝓝 x) = 𝓝 (extChartAt I x x) := by
  rw [extChartAt]
  exact map_extend_nhds_of_boundaryless (chartAt H x) (mem_chart_source H x)

Neighborhood Filter Preservation under Extended Chart for Boundaryless Models

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$ with a boundaryless model $I : H \to E$. For any point $x \in M$, the pushforward of the neighborhood filter $\mathcal{N}(x)$ under the extended chart $\text{extChartAt}_I(x)$ equals the neighborhood filter of $\text{extChartAt}_I(x)(x)$ in $E$. In other words: $$ (\text{extChartAt}_I(x))_*(\mathcal{N}(x)) = \mathcal{N}(\text{extChartAt}_I(x)(x)). $$

extChartAt_image_nhd_mem_nhds_of_mem_interior_range theorem

 {x y} (hx : y ∈ (extChartAt I x).source) (h'x : extChartAt I x y ∈ interior (range I)) {s : Set M} (h : s ∈ 𝓝 y) :
  (extChartAt I x) '' s ∈ 𝓝 (extChartAt I x y)

Full source

theorem extChartAt_image_nhd_mem_nhds_of_mem_interior_range {x y} (hx : y ∈ (extChartAt I x).source)
    (h'x : extChartAtextChartAt I x y ∈ interior (range I)) {s : Set M} (h : s ∈ 𝓝 y) :
    (extChartAt I x) '' s(extChartAt I x) '' s ∈ 𝓝 (extChartAt I x y) := by
  rw [extChartAt]
  exact extend_image_nhd_mem_nhds_of_mem_interior_range _ (by simpa using hx) h'x h

Neighborhood Preservation under Extended Chart for Interior Points

Informal description

Let $ M $ be a manifold with corners modeled on $ (E, H) $, and let $ I : H \to E $ be the model embedding. For any points $ x, y \in M $ such that $ y $ lies in the source of the extended chart $ \text{extChartAt}_I(x) $ and the image $ \text{extChartAt}_I(x)(y) $ lies in the interior of the range of $ I $, the following holds: for any neighborhood $ s $ of $ y $ in $ M $, the image of $ s $ under $ \text{extChartAt}_I(x) $ is a neighborhood of $ \text{extChartAt}_I(x)(y) $ in $ E $. In other words, if $ y \in \text{extChartAt}_I(x).\text{source} $ and $ \text{extChartAt}_I(x)(y) \in \text{interior}(\text{range}(I)) $, then for any $ s \in \mathcal{N}(y) $, we have: \[ \text{extChartAt}_I(x)(s) \in \mathcal{N}(\text{extChartAt}_I(x)(y)). \]

extChartAt_image_nhd_mem_nhds_of_boundaryless theorem

[I.Boundaryless] {x : M} (hx : s ∈ 𝓝 x) : extChartAt I x '' s ∈ 𝓝 (extChartAt I x x)

Full source

theorem extChartAt_image_nhd_mem_nhds_of_boundaryless [I.Boundaryless]
    {x : M} (hx : s ∈ 𝓝 x) : extChartAtextChartAt I x '' sextChartAt I x '' s ∈ 𝓝 (extChartAt I x x) := by
  rw [extChartAt]
  exact extend_image_nhd_mem_nhds_of_boundaryless _ (mem_chart_source H x) hx

Neighborhood Preservation under Extended Chart for Boundaryless Models

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$ with a boundaryless model $I : H \to E$. For any point $x \in M$ and any neighborhood $s$ of $x$ in $M$, the image of $s$ under the extended chart $\text{extChartAt}_I(x)$ is a neighborhood of $\text{extChartAt}_I(x)(x)$ in $E$. In other words, if $s$ is a neighborhood of $x$, then $\text{extChartAt}_I(x)(s)$ is a neighborhood of $\text{extChartAt}_I(x)(x)$ in $E$.

extChartAt_target_mem_nhdsWithin' theorem

{x y : M} (hy : y ∈ (extChartAt I x).source) : (extChartAt I x).target ∈ 𝓝[range I] extChartAt I x y

Full source

theorem extChartAt_target_mem_nhdsWithin' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    (extChartAt I x).target ∈ 𝓝[range I] extChartAt I x y :=
  extend_target_mem_nhdsWithin _ <| by rwa [← extChartAt_source I]

Neighborhood Property of Extended Chart Target Within Range at a Point

Informal description

Let $ M $ be a manifold with corners modeled on $ (E, H) $ with model embedding $ I : H \to E $. For any points $ x, y \in M $ such that $ y $ lies in the source of the extended chart $ \text{extChartAt}_I(x) $, the target of $ \text{extChartAt}_I(x) $ is a neighborhood of $ \text{extChartAt}_I(x)(y) $ within the range of $ I $. In other words: \[ (\text{extChartAt}_I(x)).\text{target} \in \mathcal{N}_{\text{extChartAt}_I(x)(y)}|_{\text{range}(I)}. \]

extChartAt_target_mem_nhdsWithin theorem

(x : M) : (extChartAt I x).target ∈ 𝓝[range I] extChartAt I x x

Full source

theorem extChartAt_target_mem_nhdsWithin (x : M) :
    (extChartAt I x).target ∈ 𝓝[range I] extChartAt I x x :=
  extChartAt_target_mem_nhdsWithin' (mem_extChartAt_source x)

Neighborhood Property of Extended Chart Target at Base Point

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ with model embedding $I: H \to E$, the target of the extended chart $\text{extChartAt}_I(x)$ is a neighborhood of $\text{extChartAt}_I(x)(x)$ within the range of $I$. In other words, there exists an open set $U \subseteq E$ containing $\text{extChartAt}_I(x)(x)$ such that $U \cap \text{range}(I) \subseteq (\text{extChartAt}_I(x)).\text{target}$.

extChartAt_target_mem_nhdsWithin_of_mem theorem

{x : M} {y : E} (hy : y ∈ (extChartAt I x).target) : (extChartAt I x).target ∈ 𝓝[range I] y

Full source

theorem extChartAt_target_mem_nhdsWithin_of_mem {x : M} {y : E} (hy : y ∈ (extChartAt I x).target) :
    (extChartAt I x).target ∈ 𝓝[range I] y := by
  rw [← (extChartAt I x).right_inv hy]
  apply extChartAt_target_mem_nhdsWithin'
  exact (extChartAt I x).map_target hy

Neighborhood Property of Extended Chart Target Within Range for Points in Target

Informal description

Let $ M $ be a manifold with corners modeled on $ (E, H) $ with model embedding $ I : H \to E $. For any point $ x \in M $ and any $ y \in E $ in the target of the extended chart $ \text{extChartAt}_I(x) $, the target set $ (\text{extChartAt}_I(x)).\text{target} $ is a neighborhood of $ y $ within the range of $ I $. In other words: \[ (\text{extChartAt}_I(x)).\text{target} \in \mathcal{N}_y|_{\text{range}(I)}. \]

extChartAt_target_union_compl_range_mem_nhds_of_mem theorem

{y : E} {x : M} (hy : y ∈ (extChartAt I x).target) : (extChartAt I x).target ∪ (range I)ᶜ ∈ 𝓝 y

Full source

theorem extChartAt_target_union_compl_range_mem_nhds_of_mem {y : E} {x : M}
    (hy : y ∈ (extChartAt I x).target) : (extChartAt I x).target ∪ (range I)ᶜ(extChartAt I x).target ∪ (range I)ᶜ ∈ 𝓝 y := by
  rw [← nhdsWithin_univ, ← union_compl_self (range I), nhdsWithin_union]
  exact Filter.union_mem_sup (extChartAt_target_mem_nhdsWithin_of_mem hy) self_mem_nhdsWithin

Neighborhood Property of Extended Chart Target Union with Complement of Range

Informal description

For any point $y$ in the target of the extended chart $\text{extChartAt}_I(x)$ at $x \in M$, the union of the chart's target with the complement of the range of $I$ is a neighborhood of $y$ in $E$. In other words: \[ (\text{extChartAt}_I(x)).\text{target} \cup (\text{range}\, I)^c \in \mathcal{N}(y). \]

isOpen_extChartAt_target theorem

[I.Boundaryless] (x : M) : IsOpen (extChartAt I x).target

Full source

/-- If we're boundaryless, `extChartAt` has open target -/
theorem isOpen_extChartAt_target [I.Boundaryless] (x : M) : IsOpen (extChartAt I x).target := by
  simp_rw [extChartAt_target, I.range_eq_univ, inter_univ]
  exact (PartialHomeomorph.open_target _).preimage I.continuous_symm

Openness of Extended Chart Target in Boundaryless Manifolds

Informal description

For a boundaryless model with corners $I$ and any point $x$ in a manifold $M$, the target of the extended chart $\text{extChartAt}_I(x)$ is an open subset of the model vector space $E$.

extChartAt_target_mem_nhds theorem

[I.Boundaryless] (x : M) : (extChartAt I x).target ∈ 𝓝 (extChartAt I x x)

Full source

/-- If we're boundaryless, `(extChartAt I x).target` is a neighborhood of the key point -/
theorem extChartAt_target_mem_nhds [I.Boundaryless] (x : M) :
    (extChartAt I x).target ∈ 𝓝 (extChartAt I x x) := by
  convert extChartAt_target_mem_nhdsWithin x
  simp only [I.range_eq_univ, nhdsWithin_univ]

Neighborhood Property of Extended Chart Target in Boundaryless Case

Informal description

For a boundaryless model with corners $I$ and any point $x$ in a manifold $M$, the target of the extended chart $\text{extChartAt}_I(x)$ is a neighborhood of $\text{extChartAt}_I(x)(x)$ in the model vector space $E$.

extChartAt_target_mem_nhds' theorem

[I.Boundaryless] {x : M} {y : E} (m : y ∈ (extChartAt I x).target) : (extChartAt I x).target ∈ 𝓝 y

Full source

/-- If we're boundaryless, `(extChartAt I x).target` is a neighborhood of any of its points -/
theorem extChartAt_target_mem_nhds' [I.Boundaryless] {x : M} {y : E}
    (m : y ∈ (extChartAt I x).target) : (extChartAt I x).target ∈ 𝓝 y :=
  (isOpen_extChartAt_target x).mem_nhds m

Extended Chart Target is Neighborhood of Any Point in Boundaryless Case

Informal description

For a boundaryless model with corners $I$, any point $x$ in a manifold $M$, and any point $y$ in the target of the extended chart $\text{extChartAt}_I(x)$, the target set $\text{extChartAt}_I(x).\text{target}$ is a neighborhood of $y$ in the model vector space $E$.

extChartAt_target_subset_range theorem

(x : M) : (extChartAt I x).target ⊆ range I

Full source

theorem extChartAt_target_subset_range (x : M) : (extChartAt I x).target ⊆ range I := by
  simp only [mfld_simps]

Extended Chart Target is Contained in Model Embedding Range

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ with corners, the target set of the extended chart $\text{extChartAt}_I(x)$ is a subset of the range of the model embedding $I \colon H \to E$.

nhdsWithin_extChartAt_target_eq' theorem

 {x y : M} (hy : y ∈ (extChartAt I x).source) :
  𝓝[(extChartAt I x).target] extChartAt I x y = 𝓝[range I] extChartAt I x y

Full source

/-- 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' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    𝓝[(extChartAt I x).target] extChartAt I x y = 𝓝[range I] extChartAt I x y :=
  nhdsWithin_extend_target_eq _ <| by rwa [← extChartAt_source I]

Equality of Neighborhood Filters for Extended Chart Target and Model Range at a Point

Informal description

For any points $x$ and $y$ in a manifold $M$ modeled on $(E, H)$ with corners, if $y$ belongs to the source of the extended chart $\text{extChartAt}_I(x)$, then the neighborhood filter of $\text{extChartAt}_I(x)(y)$ within the target of $\text{extChartAt}_I(x)$ is equal to the neighborhood filter of $\text{extChartAt}_I(x)(y)$ within the range of the model embedding $I \colon H \to E$. That is, $$\mathcal{N}_{(\text{extChartAt}_I(x)).\text{target}}(\text{extChartAt}_I(x)(y)) = \mathcal{N}_{\text{range}(I)}(\text{extChartAt}_I(x)(y)).$$

nhdsWithin_extChartAt_target_eq_of_mem theorem

{x : M} {z : E} (hz : z ∈ (extChartAt I x).target) : 𝓝[(extChartAt I x).target] z = 𝓝[range I] z

Full source

/-- 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_of_mem {x : M} {z : E} (hz : z ∈ (extChartAt I x).target) :
    𝓝[(extChartAt I x).target] z = 𝓝[range I] z := by
  rw [← PartialEquiv.right_inv (extChartAt I x) hz]
  exact nhdsWithin_extChartAt_target_eq' ((extChartAt I x).map_target hz)

Equality of Neighborhood Filters for Extended Chart Target and Model Range at a Point $z$

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ with corners, and for any point $z$ in the target of the extended chart $\text{extChartAt}_I(x)$, the neighborhood filter of $z$ within the target of $\text{extChartAt}_I(x)$ is equal to the neighborhood filter of $z$ within the range of the model embedding $I \colon H \to E$. That is, $$\mathcal{N}_{(\text{extChartAt}_I(x)).\text{target}}(z) = \mathcal{N}_{\text{range}(I)}(z).$$

nhdsWithin_extChartAt_target_eq theorem

(x : M) : 𝓝[(extChartAt I x).target] (extChartAt I x) x = 𝓝[range I] (extChartAt I x) x

Full source

/-- Around the image of the base point, the neighborhoods are the same
within `(extChartAt I x).target` and within `range I`. -/
theorem nhdsWithin_extChartAt_target_eq (x : M) :
    𝓝[(extChartAt I x).target] (extChartAt I x) x = 𝓝[range I] (extChartAt I x) x :=
  nhdsWithin_extChartAt_target_eq' (mem_extChartAt_source x)

Equality of Neighborhood Filters at Base Point in Extended Chart Target and Model Range

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ with corners, the neighborhood filter of $\text{extChartAt}_I(x)(x)$ within the target of the extended chart $\text{extChartAt}_I(x)$ is equal to the neighborhood filter of $\text{extChartAt}_I(x)(x)$ within the range of the model embedding $I \colon H \to E$. That is, $$\mathcal{N}_{(\text{extChartAt}_I(x)).\text{target}}(\text{extChartAt}_I(x)(x)) = \mathcal{N}_{\text{range}(I)}(\text{extChartAt}_I(x)(x)).$$

extChartAt_target_eventuallyEq' theorem

{x y : M} (hy : y ∈ (extChartAt I x).source) : (extChartAt I x).target =ᶠ[𝓝 (extChartAt I x y)] range I

Full source

/-- Around the image of a point in the source, `(extChartAt I x).target` and `range I`
coincide locally. -/
theorem extChartAt_target_eventuallyEq' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    (extChartAt I x).target =ᶠ[𝓝 (extChartAt I x y)] range I :=
  nhdsWithin_eq_iff_eventuallyEq.1 (nhdsWithin_extChartAt_target_eq' hy)

Local Equality of Extended Chart Target and Model Range

Informal description

For any points $x$ and $y$ in a manifold $M$ modeled on $(E, H)$ with corners, if $y$ belongs to the source of the extended chart $\text{extChartAt}_I(x)$, then the target of $\text{extChartAt}_I(x)$ is eventually equal to the range of the model embedding $I \colon H \to E$ in the neighborhood filter of $\text{extChartAt}_I(x)(y)$. In other words, there exists a neighborhood $U$ of $\text{extChartAt}_I(x)(y)$ in $E$ such that $(\text{extChartAt}_I(x)).\text{target} \cap U = \text{range}(I) \cap U$.

extChartAt_target_eventuallyEq_of_mem theorem

{x : M} {z : E} (hz : z ∈ (extChartAt I x).target) : (extChartAt I x).target =ᶠ[𝓝 z] range I

Full source

/-- Around a point in the target, `(extChartAt I x).target` and `range I` coincide locally. -/
theorem extChartAt_target_eventuallyEq_of_mem {x : M} {z : E} (hz : z ∈ (extChartAt I x).target) :
    (extChartAt I x).target =ᶠ[𝓝 z] range I :=
  nhdsWithin_eq_iff_eventuallyEq.1 (nhdsWithin_extChartAt_target_eq_of_mem hz)

Local Equality of Extended Chart Target and Model Range at a Point $z$

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ with corners, and for any point $z$ in the target of the extended chart $\text{extChartAt}_I(x)$, the target set $(\text{extChartAt}_I(x)).\text{target}$ is eventually equal to the range of the model embedding $I \colon H \to E$ in the neighborhood filter of $z$. In other words, there exists a neighborhood $U$ of $z$ in $E$ such that $(\text{extChartAt}_I(x)).\text{target} \cap U = \text{range}(I) \cap U$.

extChartAt_target_eventuallyEq theorem

{x : M} : (extChartAt I x).target =ᶠ[𝓝 (extChartAt I x x)] range I

Full source

/-- Around the image of the base point, `(extChartAt I x).target` and `range I` coincide locally. -/
theorem extChartAt_target_eventuallyEq {x : M} :
    (extChartAt I x).target =ᶠ[𝓝 (extChartAt I x x)] range I :=
  nhdsWithin_eq_iff_eventuallyEq.1 (nhdsWithin_extChartAt_target_eq x)

Local Equality of Extended Chart Target and Model Range at Base Point

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ with corners, the target of the extended chart $\text{extChartAt}_I(x)$ is eventually equal to the range of the model embedding $I \colon H \to E$ in the neighborhood filter of $\text{extChartAt}_I(x)(x)$. In other words, there exists a neighborhood $U$ of $\text{extChartAt}_I(x)(x)$ in $E$ such that $(\text{extChartAt}_I(x)).\text{target} \cap U = \text{range}(I) \cap U$.

continuousAt_extChartAt_symm'' theorem

{x : M} {y : E} (h : y ∈ (extChartAt I x).target) : ContinuousAt (extChartAt I x).symm y

Full source

theorem continuousAt_extChartAt_symm'' {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    ContinuousAt (extChartAt I x).symm y :=
  continuousAt_extend_symm' _ h

Continuity of the Inverse Extended Chart at Points in Its Target

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$, and let $\text{extChartAt}_I(x)$ be the extended chart at $x \in M$. For any point $y \in E$ in the target of $\text{extChartAt}_I(x)$, the inverse map $(\text{extChartAt}_I(x))^{-1}$ is continuous at $y$.

continuousAt_extChartAt_symm' theorem

{x x' : M} (h : x' ∈ (extChartAt I x).source) : ContinuousAt (extChartAt I x).symm (extChartAt I x x')

Full source

theorem continuousAt_extChartAt_symm' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
    ContinuousAt (extChartAt I x).symm (extChartAt I x x') :=
  continuousAt_extChartAt_symm'' <| (extChartAt I x).map_source h

Continuity of the Inverse Extended Chart at Points in Its Source

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$, and let $\text{extChartAt}_I(x)$ be the extended chart at $x \in M$. For any point $x' \in M$ in the source of $\text{extChartAt}_I(x)$, the inverse map $(\text{extChartAt}_I(x))^{-1}$ is continuous at the image point $\text{extChartAt}_I(x)(x') \in E$.

continuousAt_extChartAt_symm theorem

(x : M) : ContinuousAt (extChartAt I x).symm ((extChartAt I x) x)

Full source

theorem continuousAt_extChartAt_symm (x : M) :
    ContinuousAt (extChartAt I x).symm ((extChartAt I x) x) :=
  continuousAt_extChartAt_symm' (mem_extChartAt_source x)

Continuity of the Inverse Extended Chart at Its Image Point

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the inverse of the extended chart $\text{extChartAt}_I(x)^{-1}$ is continuous at the image point $\text{extChartAt}_I(x)(x) \in E$.

continuousOn_extChartAt_symm theorem

(x : M) : ContinuousOn (extChartAt I x).symm (extChartAt I x).target

Full source

theorem continuousOn_extChartAt_symm (x : M) :
    ContinuousOn (extChartAt I x).symm (extChartAt I x).target :=
  fun _y hy => (continuousAt_extChartAt_symm'' hy).continuousWithinAt

Continuity of the Inverse Extended Chart on Its Target

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the inverse of the extended chart $\text{extChartAt}_I(x)^{-1}$ is continuous on its target set in $E$.

extChartAt_target_subset_closure_interior theorem

{x : M} : (extChartAt I x).target ⊆ closure (interior (extChartAt I x).target)

Full source

lemma extChartAt_target_subset_closure_interior {x : M} :
    (extChartAt I x).target ⊆ closure (interior (extChartAt I x).target) := by
  intro y hy
  rw [mem_closure_iff_nhds]
  intro t ht
  have A : t ∩ ((extChartAt I x).target ∪ (range I)ᶜ)t ∩ ((extChartAt I x).target ∪ (range I)ᶜ) ∈ 𝓝 y :=
    inter_mem ht (extChartAt_target_union_compl_range_mem_nhds_of_mem hy)
  have B : y ∈ closure (interior (range I)) := by
    apply I.range_subset_closure_interior (extChartAt_target_subset_range x hy)
  obtain ⟨z, ⟨tz, h'z⟩, hz⟩ :
      (t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ)t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∩ interior (range I)).Nonempty :=
    mem_closure_iff_nhds.1 B _ A
  refine ⟨z, ⟨tz, ?_⟩⟩
  have h''z : z ∈ (extChartAt I x).target := by simpa [interior_subset hz] using h'z
  exact (extChartAt_target_eventuallyEq_of_mem h''z).symm.mem_interior hz

Extended Chart Target is Contained in Closure of Interior

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ with corners, the target of the extended chart $\text{extChartAt}_I(x)$ is contained in the closure of its interior, i.e., \[ (\text{extChartAt}_I(x)).\text{target} \subseteq \overline{\text{interior}((\text{extChartAt}_I(x)).\text{target})}. \]

interior_extChartAt_target_nonempty theorem

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

Full source

theorem interior_extChartAt_target_nonempty (x : M) :
    (interior (extChartAt I x).target).Nonempty := by
  by_contra! H
  have := extChartAt_target_subset_closure_interior (mem_extChartAt_target (I := I) x)
  simp only [H, closure_empty, mem_empty_iff_false] at this

Nonempty Interior of Extended Chart Target

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ with corners, the interior of the target set of the extended chart $\text{extChartAt}_I(x)$ is nonempty.

extChartAt_mem_closure_interior theorem

 {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))

Full source

lemma extChartAt_mem_closure_interior {x₀ x : M}
    (hx : x ∈ closure (interior s)) (h'x : x ∈ (extChartAt I x₀).source) :
    extChartAtextChartAt I x₀ x ∈
      closure (interior ((extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target)) := by
  simp_rw [mem_closure_iff, interior_inter, ← inter_assoc]
  intro o o_open ho
  obtain ⟨y, ⟨yo, hy⟩, ys⟩ :
      ((extChartAt I x₀) ⁻¹' o(extChartAt I x₀) ⁻¹' o ∩ (extChartAt I x₀).source(extChartAt I x₀) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty := by
    have : (extChartAt I x₀) ⁻¹' o(extChartAt I x₀) ⁻¹' o ∈ 𝓝 x := by
      apply (continuousAt_extChartAt' h'x).preimage_mem_nhds (o_open.mem_nhds ho)
    refine (mem_closure_iff_nhds.1 hx) _ (inter_mem this ?_)
    apply (isOpen_extChartAt_source x₀).mem_nhds h'x
  have A : interiorinterior (↑(extChartAt I x₀).symm ⁻¹' s) ∈ 𝓝 (extChartAt I x₀ y) := by
    simp only [interior_mem_nhds]
    apply (continuousAt_extChartAt_symm' hy).preimage_mem_nhds
    simp only [hy, PartialEquiv.left_inv]
    exact mem_interior_iff_mem_nhds.mp ys
  have B : (extChartAt I x₀) y ∈ closure (interior (extChartAt I x₀).target) := by
    apply extChartAt_target_subset_closure_interior (x := x₀)
    exact (extChartAt I x₀).map_source hy
  exact mem_closure_iff_nhds.1 B _ (inter_mem (o_open.mem_nhds yo) A)

Image under Extended Chart Belongs to Closure of Interior of Preimage Intersection

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$, and let $x_0, x \in M$ be points such that $x$ belongs to the closure of the interior of a subset $s \subseteq M$ and $x$ is in the source of the extended chart $\text{extChartAt}_I(x_0)$. Then the image of $x$ under $\text{extChartAt}_I(x_0)$ belongs to the closure of the interior of the set obtained by intersecting the preimage of $s$ under the inverse extended chart with the target of $\text{extChartAt}_I(x_0)$. In other words, under the given conditions, we have: \[ \text{extChartAt}_I(x_0)(x) \in \overline{\text{interior}\left((\text{extChartAt}_I(x_0))^{-1}(s) \cap (\text{extChartAt}_I(x_0)).\text{target}\right)}. \]

isOpen_extChartAt_preimage' theorem

(x : M) {s : Set E} (hs : IsOpen s) : IsOpen ((extChartAt I x).source ∩ extChartAt I x ⁻¹' s)

Full source

theorem isOpen_extChartAt_preimage' (x : M) {s : Set E} (hs : IsOpen s) :
    IsOpen ((extChartAt I x).source ∩ extChartAt I x ⁻¹' s) :=
  isOpen_extend_preimage' _ hs

Openness of Preimage under Extended Chart at a Point

Informal description

Let $ M $ be a smooth manifold with corners modeled on $ (E, H) $ via the model with corners $ I $. For any point $ x \in M $ and any open subset $ s \subseteq E $, the intersection of the source of the extended chart $ \text{extChartAt}_I(x) $ with the preimage of $ s $ under $ \text{extChartAt}_I(x) $ is an open subset of $ M $. In other words, if $ s $ is open in $ E $, then $ (\text{extChartAt}_I(x))^{-1}(s) \cap \text{dom}(\text{extChartAt}_I(x)) $ is open in $ M $.

isOpen_extChartAt_preimage theorem

(x : M) {s : Set E} (hs : IsOpen s) : IsOpen ((chartAt H x).source ∩ extChartAt I x ⁻¹' s)

Full source

theorem isOpen_extChartAt_preimage (x : M) {s : Set E} (hs : IsOpen s) :
    IsOpen ((chartAt H x).source ∩ extChartAt I x ⁻¹' s) := by
  rw [← extChartAt_source I]
  exact isOpen_extChartAt_preimage' x hs

Openness of Preimage under Extended Chart at a Point Relative to Chart Source

Informal description

Let $ M $ be a smooth manifold with corners modeled on $ (E, H) $ via the model with corners $ I $. For any point $ x \in M $ and any open subset $ s \subseteq E $, the intersection of the source of the chart $ \text{chartAt}_H(x) $ with the preimage of $ s $ under the extended chart $ \text{extChartAt}_I(x) $ is an open subset of $ M $. In other words, if $ s $ is open in $ E $, then $ (\text{extChartAt}_I(x))^{-1}(s) \cap \text{dom}(\text{chartAt}_H(x)) $ is open in $ M $.

map_extChartAt_nhdsWithin_eq_image' theorem

 {x y : M} (hy : y ∈ (extChartAt I x).source) :
  map (extChartAt I x) (𝓝[s] y) = 𝓝[extChartAt I x '' ((extChartAt I x).source ∩ s)] extChartAt I x y

Full source

theorem map_extChartAt_nhdsWithin_eq_image' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    map (extChartAt I x) (𝓝[s] y) =
      𝓝[extChartAt I x '' ((extChartAt I x).source ∩ s)] extChartAt I x y :=
  map_extend_nhdsWithin_eq_image _ <| by rwa [← extChartAt_source I]

Equality of Neighborhood Filters under Extended Chart Mapping at a Point

Informal description

Let $ M $ be a smooth manifold with corners modeled on $ (E, H ) $ via the model with corners $ I $. For any points $ x, y \in M $ such that $ y $ belongs to the source of the extended chart $ \text{extChartAt}_I(x) $, and for any subset $ s \subseteq M $, the image under $ \text{extChartAt}_I(x) $ of the neighborhood filter of $ y $ within $ s $ equals the neighborhood filter of $ \text{extChartAt}_I(x)(y) $ within the image of the intersection of the source of $ \text{extChartAt}_I(x) $ with $ s $. In other words, for $ y \in \text{source}(\text{extChartAt}_I(x)) $, we have: \[ \text{extChartAt}_I(x)_*(\mathcal{N}_s(y)) = \mathcal{N}_{\text{extChartAt}_I(x)(\text{source}(\text{extChartAt}_I(x)) \cap s)}(\text{extChartAt}_I(x)(y)) \]

map_extChartAt_nhdsWithin_eq_image theorem

(x : M) : map (extChartAt I x) (𝓝[s] x) = 𝓝[extChartAt I x '' ((extChartAt I x).source ∩ s)] extChartAt I x x

Full source

theorem map_extChartAt_nhdsWithin_eq_image (x : M) :
    map (extChartAt I x) (𝓝[s] x) =
      𝓝[extChartAt I x '' ((extChartAt I x).source ∩ s)] extChartAt I x x :=
  map_extChartAt_nhdsWithin_eq_image' (mem_extChartAt_source x)

Equality of Neighborhood Filters under Extended Chart Mapping at a Point within a Subset

Informal description

Let $ M $ be a smooth manifold with corners modeled on $ (E, H) $ via the model with corners $ I $. For any point $ x \in M $ and any subset $ s \subseteq M $, the image under the extended chart $ \text{extChartAt}_I(x) $ of the neighborhood filter of $ x $ within $ s $ equals the neighborhood filter of $ \text{extChartAt}_I(x)(x) $ within the image of the intersection of the source of $ \text{extChartAt}_I(x) $ with $ s $. In other words, we have: \[ \text{extChartAt}_I(x)_*(\mathcal{N}_s(x)) = \mathcal{N}_{\text{extChartAt}_I(x)(\text{source}(\text{extChartAt}_I(x)) \cap s)}(\text{extChartAt}_I(x)(x)) \]

map_extChartAt_nhdsWithin' theorem

 {x y : M} (hy : y ∈ (extChartAt I x).source) :
  map (extChartAt I x) (𝓝[s] y) = 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x y

Full source

theorem map_extChartAt_nhdsWithin' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    map (extChartAt I x) (𝓝[s] y) = 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x y :=
  map_extend_nhdsWithin _ <| by rwa [← extChartAt_source I]

Equality of Neighborhood Filters under Extended Chart Mapping with Preimage Condition at a Point

Informal description

Let $ M $ be a smooth manifold with corners modeled on $ (E, H) $ via the model with corners $ I $. For any points $ x, y \in M $ such that $ y $ belongs to the source of the extended chart $ \text{extChartAt}_I(x) $, and for any subset $ s \subseteq M $, the image under $ \text{extChartAt}_I(x) $ of the neighborhood filter of $ y $ within $ s $ equals the neighborhood filter of $ \text{extChartAt}_I(x)(y) $ within the intersection of the preimage of $ s $ under the inverse of $ \text{extChartAt}_I(x) $ and the range of $ I $. In other words, for $ y \in \text{source}(\text{extChartAt}_I(x)) $, we have: \[ \text{extChartAt}_I(x)_*(\mathcal{N}_s(y)) = \mathcal{N}_{(\text{extChartAt}_I(x)^{-1}(s)) \cap \text{range}(I)}(\text{extChartAt}_I(x)(y)) \]

map_extChartAt_nhdsWithin theorem

(x : M) : map (extChartAt I x) (𝓝[s] x) = 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x x

Full source

theorem map_extChartAt_nhdsWithin (x : M) :
    map (extChartAt I x) (𝓝[s] x) = 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x x :=
  map_extChartAt_nhdsWithin' (mem_extChartAt_source x)

Neighborhood Filter Equality under Extended Chart Mapping within a Subset

Informal description

Let $ M $ be a smooth manifold with corners modeled on $ (E, H) $ via the model with corners $ I $. For any point $ x \in M $ and any subset $ s \subseteq M $, the image under the extended chart $ \text{extChartAt}_I(x) $ of the neighborhood filter of $ x $ within $ s $ equals the neighborhood filter of $ \text{extChartAt}_I(x)(x) $ within the intersection of the preimage of $ s $ under the inverse of $ \text{extChartAt}_I(x) $ and the range of $ I $. In other words, we have: \[ \text{extChartAt}_I(x)_*(\mathcal{N}_s(x)) = \mathcal{N}_{(\text{extChartAt}_I(x)^{-1}(s)) \cap \text{range}(I)}(\text{extChartAt}_I(x)(x)) \]

map_extChartAt_symm_nhdsWithin' theorem

 {x y : M} (hy : y ∈ (extChartAt I x).source) :
  map (extChartAt I x).symm (𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x y) = 𝓝[s] y

Full source

theorem map_extChartAt_symm_nhdsWithin' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    map (extChartAt I x).symm (𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x y) =
      𝓝[s] y :=
  map_extend_symm_nhdsWithin _ <| by rwa [← extChartAt_source I]

Inverse Extended Chart Preserves Neighborhood Filters with Preimage Condition at a Point

Informal description

Let $ M $ be a smooth manifold with corners modeled on $ (E, H) $ via the model with corners $ I $. For any points $ x, y \in M $ such that $ y $ belongs to the source of the extended chart $ \text{extChartAt}_I(x) $, and for any subset $ s \subseteq M $, the image under the inverse of $ \text{extChartAt}_I(x) $ of the neighborhood filter of $ \text{extChartAt}_I(x)(y) $ within the intersection of the preimage of $ s $ under the inverse of $ \text{extChartAt}_I(x) $ and the range of $ I $, equals the neighborhood filter of $ y $ within $ s $. In other words, for $ y \in \text{source}(\text{extChartAt}_I(x)) $, we have: \[ (\text{extChartAt}_I(x)^{-1})_*(\mathcal{N}_{(\text{extChartAt}_I(x)^{-1}(s)) \cap \text{range}(I)}(\text{extChartAt}_I(x)(y))) = \mathcal{N}_s(y). \]

map_extChartAt_symm_nhdsWithin_range' theorem

{x y : M} (hy : y ∈ (extChartAt I x).source) : map (extChartAt I x).symm (𝓝[range I] extChartAt I x y) = 𝓝 y

Full source

theorem map_extChartAt_symm_nhdsWithin_range' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    map (extChartAt I x).symm (𝓝[range I] extChartAt I x y) = 𝓝 y :=
  map_extend_symm_nhdsWithin_range _ <| by rwa [← extChartAt_source I]

Inverse Extended Chart Preserves Neighborhood Filters within Range at a Point

Informal description

Let $ M $ be a smooth manifold with corners modeled on $ (E, H) $ via the model with corners $ I $. For any points $ x, y \in M $ such that $ y $ belongs to the domain of the extended chart $ \text{extChartAt}_I(x) $, the image under the inverse of $ \text{extChartAt}_I(x) $ of the neighborhood filter of $ \text{extChartAt}_I(x)(y) $ within the range of $ I $ equals the neighborhood filter of $ y $. In other words, for $ y \in \text{source}(\text{extChartAt}_I(x)) $, we have: \[ (\text{extChartAt}_I(x)^{-1})_*(\mathcal{N}_{\text{range}(I)}(\text{extChartAt}_I(x)(y))) = \mathcal{N}(y). \]

map_extChartAt_symm_nhdsWithin theorem

(x : M) : map (extChartAt I x).symm (𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x x) = 𝓝[s] x

Full source

theorem map_extChartAt_symm_nhdsWithin (x : M) :
    map (extChartAt I x).symm (𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x x) =
      𝓝[s] x :=
  map_extChartAt_symm_nhdsWithin' (mem_extChartAt_source x)

Inverse Extended Chart Preserves Neighborhood Filters at a Point within a Subset

Informal description

Let $ M $ be a smooth manifold with corners modeled on $ (E, H) $ via the model with corners $ I $. For any point $ x \in M $ and any subset $ s \subseteq M $, the image under the inverse of the extended chart $ \text{extChartAt}_I(x) $ of the neighborhood filter of $ \text{extChartAt}_I(x)(x) $ within the intersection of the preimage of $ s $ under the inverse of $ \text{extChartAt}_I(x) $ and the range of $ I $, equals the neighborhood filter of $ x $ within $ s $. In other words, for $ x \in \text{source}(\text{extChartAt}_I(x)) $, we have: \[ (\text{extChartAt}_I(x)^{-1})_*(\mathcal{N}_{(\text{extChartAt}_I(x)^{-1}(s)) \cap \text{range}(I)}(\text{extChartAt}_I(x)(x))) = \mathcal{N}_s(x). \]

map_extChartAt_symm_nhdsWithin_range theorem

(x : M) : map (extChartAt I x).symm (𝓝[range I] extChartAt I x x) = 𝓝 x

Full source

theorem map_extChartAt_symm_nhdsWithin_range (x : M) :
    map (extChartAt I x).symm (𝓝[range I] extChartAt I x x) = 𝓝 x :=
  map_extChartAt_symm_nhdsWithin_range' (mem_extChartAt_source x)

Inverse Extended Chart Preserves Neighborhood Filters within Range at Base Point

Informal description

Let $ M $ be a smooth manifold with corners modeled on $ (E, H) $ via the model with corners $ I $. For any point $ x \in M $, the image under the inverse of the extended chart $ \text{extChartAt}_I(x) $ of the neighborhood filter of $ \text{extChartAt}_I(x)(x) $ within the range of $ I $ equals the neighborhood filter of $ x $. In other words, for $ x \in M $, we have: \[ (\text{extChartAt}_I(x)^{-1})_*(\mathcal{N}_{\text{range}(I)}(\text{extChartAt}_I(x)(x))) = \mathcal{N}(x). \]

extChartAt_preimage_mem_nhdsWithin' theorem

 {x x' : M} (h : x' ∈ (extChartAt I x).source) (ht : t ∈ 𝓝[s] x') :
  (extChartAt I x).symm ⁻¹' t ∈ 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x'

Full source

/-- 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' {x x' : M} (h : x' ∈ (extChartAt I x).source)
    (ht : t ∈ 𝓝[s] x') :
    (extChartAt I x).symm ⁻¹' t(extChartAt I x).symm ⁻¹' t ∈ 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x' := by
  rwa [← map_extChartAt_symm_nhdsWithin' h, mem_map] at ht

Neighborhood Preservation Under Inverse Extended Chart Within a Set

Informal description

Let $ M $ be a smooth manifold with corners modeled on $ (E, H) $ via the model with corners $ I $. For any points $ x, x' \in M $ such that $ x' $ belongs to the source of the extended chart $ \text{extChartAt}_I(x) $, and for any subset $ s \subseteq M $, if $ t $ is a neighborhood of $ x' $ within $ s $, then the preimage of $ t $ under the inverse of $ \text{extChartAt}_I(x) $ is a neighborhood of $ \text{extChartAt}_I(x)(x') $ within the intersection of the preimage of $ s $ under the inverse of $ \text{extChartAt}_I(x) $ and the range of $ I $. In other words, for $ x' \in \text{source}(\text{extChartAt}_I(x)) $ and $ t \in \mathcal{N}_s(x') $, we have: \[ (\text{extChartAt}_I(x)^{-1})^{-1}(t) \in \mathcal{N}_{(\text{extChartAt}_I(x)^{-1}(s)) \cap \text{range}(I)}(\text{extChartAt}_I(x)(x')). \]

extChartAt_preimage_mem_nhdsWithin theorem

 {x : M} (ht : t ∈ 𝓝[s] x) : (extChartAt I x).symm ⁻¹' t ∈ 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x

Full source

/-- 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_nhdsWithin {x : M} (ht : t ∈ 𝓝[s] x) :
    (extChartAt I x).symm ⁻¹' t(extChartAt I x).symm ⁻¹' t ∈ 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x :=
  extChartAt_preimage_mem_nhdsWithin' (mem_extChartAt_source x) ht

Neighborhood Preservation Under Inverse Extended Chart Within a Set at Base Point

Informal description

Let $M$ be a smooth manifold with corners modeled on $(E, H)$ via the model with corners $I$. For any point $x \in M$ and any neighborhood $t$ of $x$ within a subset $s \subseteq M$, the preimage of $t$ under the inverse of the extended chart $\text{extChartAt}_I(x)^{-1}$ is a neighborhood of $\text{extChartAt}_I(x)(x)$ within the intersection of the preimage of $s$ under $\text{extChartAt}_I(x)^{-1}$ and the range of $I$. In other words, for $t \in \mathcal{N}_s(x)$, we have: \[ (\text{extChartAt}_I(x)^{-1})^{-1}(t) \in \mathcal{N}_{(\text{extChartAt}_I(x)^{-1}(s)) \cap \text{range}(I)}(\text{extChartAt}_I(x)(x)). \]

extChartAt_preimage_mem_nhds' theorem

 {x x' : M} (h : x' ∈ (extChartAt I x).source) (ht : t ∈ 𝓝 x') : (extChartAt I x).symm ⁻¹' t ∈ 𝓝 (extChartAt I x x')

Full source

theorem extChartAt_preimage_mem_nhds' {x x' : M} (h : x' ∈ (extChartAt I x).source)
    (ht : t ∈ 𝓝 x') : (extChartAt I x).symm ⁻¹' t(extChartAt I x).symm ⁻¹' t ∈ 𝓝 (extChartAt I x x') :=
  extend_preimage_mem_nhds _ (by rwa [← extChartAt_source I]) ht

Neighborhood preservation under inverse extended chart at a point

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$, and let $x, x' \in M$ with $x'$ in the domain of the extended chart $\text{extChartAt}_I(x)$. For any neighborhood $t$ of $x'$ in $M$, the preimage of $t$ under the inverse of the extended chart $(\text{extChartAt}_I(x))^{-1}$ is a neighborhood of $\text{extChartAt}_I(x)(x')$ in $E$.

extChartAt_preimage_mem_nhds theorem

{x : M} (ht : t ∈ 𝓝 x) : (extChartAt I x).symm ⁻¹' t ∈ 𝓝 ((extChartAt I x) x)

Full source

/-- 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_mem_nhds {x : M} (ht : t ∈ 𝓝 x) :
    (extChartAt I x).symm ⁻¹' t(extChartAt I x).symm ⁻¹' t ∈ 𝓝 ((extChartAt I x) x) := by
  apply (continuousAt_extChartAt_symm x).preimage_mem_nhds
  rwa [(extChartAt I x).left_inv (mem_extChartAt_source _)]

Neighborhood preservation under inverse extended chart

Informal description

Let $M$ be a manifold with corners modeled on $(E, H)$. For any point $x \in M$ and any neighborhood $t$ of $x$ in $M$, the preimage of $t$ under the inverse of the extended chart $\text{extChartAt}_I(x)^{-1}$ is a neighborhood of $\text{extChartAt}_I(x)(x)$ in $E$.

extChartAt_preimage_inter_eq theorem

 (x : M) :
  (extChartAt I x).symm ⁻¹' (s ∩ t) ∩ range I = (extChartAt I x).symm ⁻¹' s ∩ range I ∩ (extChartAt I x).symm ⁻¹' t

Full source

/-- 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 extChartAt_preimage_inter_eq (x : M) :
    (extChartAt I x).symm ⁻¹' (s ∩ t)(extChartAt I x).symm ⁻¹' (s ∩ t) ∩ range I =
      (extChartAt I x).symm ⁻¹' s(extChartAt I x).symm ⁻¹' s ∩ range I(extChartAt I x).symm ⁻¹' s ∩ range I ∩ (extChartAt I x).symm ⁻¹' t := by
  mfld_set_tac

Preimage of Intersection under Inverse Extended Chart Equals Intersection of Preimages

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, the preimage under the inverse extended chart $\text{extChartAt}_I(x)^{-1}$ of the intersection $s \cap t$ intersected with the range of the model embedding $I$ equals the intersection of the preimage of $s$ and the range of $I$ with the preimage of $t$. More precisely: $$(\text{extChartAt}_I(x)^{-1})^{-1}(s \cap t) \cap \text{range}(I) = (\text{extChartAt}_I(x)^{-1})^{-1}(s) \cap \text{range}(I) \cap (\text{extChartAt}_I(x)^{-1})^{-1}(t)$$

ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range theorem

 {f : M → M'} {x : M} (hc : ContinuousWithinAt f s x) :
  𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x x) =
    𝓝[(extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)] (extChartAt I x x)

Full source

theorem ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range
    {f : M → M'} {x : M} (hc : ContinuousWithinAt f s x) :
    𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x x) =
      𝓝[(extChartAt I x).target ∩
        (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)] (extChartAt I x x) := by
  rw [← (extChartAt I x).image_source_inter_eq', ← map_extChartAt_nhdsWithin_eq_image,
    ← map_extChartAt_nhdsWithin, nhdsWithin_inter_of_mem']
  exact hc (extChartAt_source_mem_nhds _)

Equality of Neighborhood Filters under Extended Chart Mapping for Continuous Functions on Manifolds with Corners

Informal description

Let $M$ and $M'$ be smooth manifolds with corners modeled on $(E, H)$ and $(E', H')$ respectively, via model embeddings $I$ and $I'$. Let $f \colon M \to M'$ be a continuous function within a subset $s \subseteq M$ at a point $x \in M$. Then the neighborhood filter of $\text{extChartAt}_I(x)(x)$ within the intersection of the preimage of $s$ under $\text{extChartAt}_I(x)^{-1}$ and the range of $I$ is equal to the neighborhood filter of $\text{extChartAt}_I(x)(x)$ within the intersection of the target of $\text{extChartAt}_I(x)$ and the preimage of $s \cap f^{-1}(\text{extChartAt}_{I'}(f(x)).\text{source})$ under $\text{extChartAt}_I(x)^{-1}$. In other words: \[ \mathcal{N}_{(\text{extChartAt}_I(x)^{-1}(s)) \cap \text{range}(I)}(\text{extChartAt}_I(x)(x)) = \mathcal{N}_{\text{extChartAt}_I(x).\text{target} \cap \text{extChartAt}_I(x)^{-1}(s \cap f^{-1}(\text{extChartAt}_{I'}(f(x)).\text{source}))}(\text{extChartAt}_I(x)(x)) \]

ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq theorem

 {f : M → M'} {x : M} (hc : ContinuousWithinAt f s x) :
  ((extChartAt I x).symm ⁻¹' s ∩ range I : Set E) =ᶠ[𝓝 (extChartAt I x x)]
    ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) : Set E)

Full source

theorem ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq
    {f : M → M'} {x : M} (hc : ContinuousWithinAt f s x) :
    ((extChartAt I x).symm ⁻¹' s ∩ range I : Set E) =ᶠ[𝓝 (extChartAt I x x)]
      ((extChartAt I x).target ∩
        (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) : Set E) := by
  rw [← nhdsWithin_eq_iff_eventuallyEq]
  exact hc.nhdsWithin_extChartAt_symm_preimage_inter_range

Eventual Equality of Preimage Sets under Extended Chart for Continuous Functions on Manifolds with Corners

Informal description

Let $M$ and $M'$ be smooth manifolds with corners modeled on $(E, H)$ and $(E', H')$ respectively, via model embeddings $I$ and $I'$. Let $f \colon M \to M'$ be a function that is continuous within a subset $s \subseteq M$ at a point $x \in M$. Then, in the model space $E$, the intersection of the preimage of $s$ under the inverse extended chart $\text{extChartAt}_I(x)^{-1}$ with the range of $I$ is eventually equal (in the neighborhood filter of $\text{extChartAt}_I(x)(x)$) to the intersection of the target of $\text{extChartAt}_I(x)$ with the preimage of $s \cap f^{-1}(\text{extChartAt}_{I'}(f(x)).\text{source})$ under $\text{extChartAt}_I(x)^{-1}$. In other words: \[ (\text{extChartAt}_I(x)^{-1}(s) \cap \text{range}(I)) =_{\mathcal{N}(\text{extChartAt}_I(x)(x))} (\text{extChartAt}_I(x).\text{target} \cap \text{extChartAt}_I(x)^{-1}(s \cap f^{-1}(\text{extChartAt}_{I'}(f(x)).\text{source}))) \]

ext_coord_change_source theorem

(x x' : M) : ((extChartAt I x').symm ≫ extChartAt I x).source = I '' ((chartAt H x').symm ≫ₕ chartAt H x).source

Full source

theorem ext_coord_change_source (x x' : M) :
    ((extChartAt I x').symm ≫ extChartAt I x).source =
      I '' ((chartAt H x').symm ≫ₕ chartAt H x).source :=
  extend_coord_change_source _ _

Source of Extended Coordinate Change Equals Image of Original Coordinate Change Source

Informal description

For any two points $x$ and $x'$ in a manifold $M$ modeled on $(E, H)$, the source of the extended coordinate change between the extended charts at $x$ and $x'$ equals the image under the model embedding $I : H \to E$ of the source of the coordinate change between the original charts at $x$ and $x'$. More precisely, let $\text{extChartAt}_I(x)$ and $\text{extChartAt}_I(x')$ be the extended charts at $x$ and $x'$ respectively, obtained by composing the original charts with $I$. Then: $$\text{source}\left((\text{extChartAt}_I(x'))^{-1} \circ \text{extChartAt}_I(x)\right) = I\left(\text{source}\left((\text{chartAt}_H(x'))^{-1} \circ \text{chartAt}_H(x)\right)\right)$$

contDiffOn_ext_coord_change theorem

 [IsManifold I n M] (x x' : M) :
  ContDiffOn 𝕜 n (extChartAt I x ∘ (extChartAt I x').symm) ((extChartAt I x').symm ≫ extChartAt I x).source

Full source

theorem contDiffOn_ext_coord_change [IsManifold I n M] (x x' : M) :
    ContDiffOn 𝕜 n (extChartAtextChartAt I x ∘ (extChartAt I x').symm)
      ((extChartAt I x').symm ≫ extChartAt I x).source :=
  contDiffOn_extend_coord_change (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x')

$C^n$-Differentiability of Extended Chart Coordinate Changes on Manifolds with Corners

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$ with embedding $I : H \to E$. For any two points $x, x' \in M$, the coordinate change map between their extended charts, given by $\text{extChartAt}_I(x) \circ (\text{extChartAt}_I(x'))^{-1}$, is $C^n$-differentiable on its domain of definition (the source of the composition $(\text{extChartAt}_I(x'))^{-1} \circ \text{extChartAt}_I(x)$).

contDiffWithinAt_ext_coord_change theorem

 [IsManifold I n M] (x x' : M) {y : E} (hy : y ∈ ((extChartAt I x').symm ≫ extChartAt I x).source) :
  ContDiffWithinAt 𝕜 n (extChartAt I x ∘ (extChartAt I x').symm) (range I) y

Full source

theorem contDiffWithinAt_ext_coord_change [IsManifold I n M] (x x' : M) {y : E}
    (hy : y ∈ ((extChartAt I x').symm ≫ extChartAt I x).source) :
    ContDiffWithinAt 𝕜 n (extChartAtextChartAt I x ∘ (extChartAt I x').symm) (range I) y :=
  contDiffWithinAt_extend_coord_change (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x') hy

$C^n$-Differentiability of Extended Chart Coordinate Changes at a Point

Informal description

Let $M$ be a $C^n$ manifold with corners modeled on $(E, H)$ with embedding $I : H \to E$. For any two points $x, x' \in M$ and any point $y \in E$ in the domain of the extended coordinate change $(\text{extChartAt}_I(x'))^{-1} \circ \text{extChartAt}_I(x)$, the composition $\text{extChartAt}_I(x) \circ (\text{extChartAt}_I(x'))^{-1}$ is $C^n$-differentiable at $y$ within the range of $I$.

writtenInExtChartAt definition

(x : M) (f : M → M') : E → E'

Full source

/-- 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. -/
@[simp, mfld_simps]
def writtenInExtChartAt (x : M) (f : M → M') : E → E' :=
  extChartAtextChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm

Local representation of a function in extended charts

Informal description

Given a point $ x $ in a manifold $ M $ modeled on $ (E, H) $ and a function $ f : M \to M' $ between manifolds, the function $ \text{writtenInExtChartAt}_I^{I'}(x, f) $ is the representation of $ f $ in the extended charts around $ x $ and $ f(x) $. Specifically, it is the composition of the extended chart at $ f(x) $ in $ M' $, the function $ f $, and the inverse of the extended chart at $ x $ in $ M $, yielding a map from $ E $ to $ E' $. More precisely, for $ y \in E $ in the target of the extended chart at $ x $, the function is defined as: \[ \text{writtenInExtChartAt}_I^{I'}(x, f)(y) = \text{extChartAt}_{I'}(f(x)) \circ f \circ (\text{extChartAt}_I(x))^{-1}(y). \] This construction allows the study of $ f $ locally in the model vector spaces $ E $ and $ E' $, facilitating the computation of derivatives and other local properties.

writtenInExtChartAt_chartAt theorem

{x : M} {y : E} (h : y ∈ (extChartAt I x).target) : writtenInExtChartAt I I x (chartAt H x) y = y

Full source

theorem writtenInExtChartAt_chartAt {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    writtenInExtChartAt I I x (chartAt H x) y = y := by simp_all only [mfld_simps]

Identity Property of Local Chart Representation in Extended Charts

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ and any $y \in E$ in the target of the extended chart at $x$, the local representation of the chart $\text{chartAt}_H(x)$ in the extended charts satisfies $\text{writtenInExtChartAt}_I^I(x, \text{chartAt}_H(x))(y) = y$.

writtenInExtChartAt_chartAt_symm theorem

{x : M} {y : E} (h : y ∈ (extChartAt I x).target) : writtenInExtChartAt I I (chartAt H x x) (chartAt H x).symm y = y

Full source

theorem writtenInExtChartAt_chartAt_symm {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    writtenInExtChartAt I I (chartAt H x x) (chartAt H x).symm y = y := by
  simp_all only [mfld_simps]

Identity Property of Inverse Chart Representation in Extended Charts

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ and any $y \in E$ in the target of the extended chart at $x$, the local representation of the inverse chart $\text{chartAt}_H(x)^{-1}$ in the extended charts satisfies: \[ \text{writtenInExtChartAt}_I^I(\text{chartAt}_H(x)(x), \text{chartAt}_H(x)^{-1})(y) = y. \]

writtenInExtChartAt_extChartAt theorem

{x : M} {y : E} (h : y ∈ (extChartAt I x).target) : writtenInExtChartAt I 𝓘(𝕜, E) x (extChartAt I x) y = y

Full source

theorem writtenInExtChartAt_extChartAt {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    writtenInExtChartAt I 𝓘(𝕜, E) x (extChartAt I x) y = y := by
  simp_all only [mfld_simps]

Identity Property of Extended Chart Representation in Itself

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$ and any $y \in E$ in the target of the extended chart at $x$, the local representation of the extended chart $\text{extChartAt}_I(x)$ in itself satisfies $\text{writtenInExtChartAt}_I^{\mathcal{I}(\mathbb{K}, E)}(x, \text{extChartAt}_I(x))(y) = y$.

writtenInExtChartAt_extChartAt_symm theorem

 {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
  writtenInExtChartAt 𝓘(𝕜, E) I (extChartAt I x x) (extChartAt I x).symm y = y

Full source

theorem writtenInExtChartAt_extChartAt_symm {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    writtenInExtChartAt 𝓘(𝕜, E) I (extChartAt I x x) (extChartAt I x).symm y = y := by
  simp_all only [mfld_simps]

Identity Property of Extended Chart Composition in Model Vector Space

Informal description

For any point $x$ in a manifold $M$ modeled on $(E, H)$, and any point $y$ in the target of the extended chart $\text{extChartAt}_I(x)$, the composition of the extended chart at $x$ with its inverse, when written in the extended charts, equals the identity on $y$. More precisely, if $y$ belongs to the target of $\text{extChartAt}_I(x)$, then: \[ \text{writtenInExtChartAt}_{\mathcal{I}(\mathbb{K}, E)}^I \left( \text{extChartAt}_I(x)(x), (\text{extChartAt}_I(x))^{-1} \right)(y) = y. \] Here, $\mathcal{I}(\mathbb{K}, E)$ denotes the trivial model with corners on $E$.

extChartAt_self_eq theorem

{x : H} : ⇑(extChartAt I x) = I

Full source

theorem extChartAt_self_eq {x : H} : ⇑(extChartAt I x) = I :=
  rfl

Extended Chart Coincides with Model Embedding on Model Space

Informal description

For any point $x$ in the model space $H$, the extended chart $\text{extChartAt}_I(x)$ coincides with the model embedding $I : H \to E$ as functions.

extChartAt_self_apply theorem

{x y : H} : extChartAt I x y = I y

Full source

theorem extChartAt_self_apply {x y : H} : extChartAt I x y = I y :=
  rfl

Extended Chart at a Point in Model Space Equals Model Embedding

Informal description

For any points $x, y$ in the model space $H$, the extended chart at $x$ evaluated at $y$ equals the model embedding $I$ evaluated at $y$, i.e., $\text{extChartAt}_I(x)(y) = I(y)$.

extChartAt_model_space_eq_id theorem

(x : E) : extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E

Full source

/-- In the case of the manifold structure on a vector space, the extended charts are just the
identity. -/
theorem extChartAt_model_space_eq_id (x : E) : extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E := by
  simp only [mfld_simps]

Extended Chart as Identity in Model Space

Informal description

For any point $x$ in a normed vector space $E$ over a nontrivially normed field $\mathbb{K}$, the extended chart at $x$ with respect to the trivial model with corners structure $\mathcal{I}(\mathbb{K}, E)$ is equal to the identity partial equivalence on $E$.

ext_chart_model_space_apply theorem

{x y : E} : extChartAt 𝓘(𝕜, E) x y = y

Full source

theorem ext_chart_model_space_apply {x y : E} : extChartAt 𝓘(𝕜, E) x y = y :=
  rfl

Extended Chart on Model Space Acts as Identity: $\text{extChartAt}_{\mathcal{I}(\mathbb{K}, E)}(x)(y) = y$

Informal description

For any points $x, y$ in the model vector space $E$ of a manifold with the trivial model with corners structure $\mathcal{I}(\mathbb{K}, E)$, the extended chart $\text{extChartAt}_{\mathcal{I}(\mathbb{K}, E)}(x)$ evaluated at $y$ is equal to $y$.

extChartAt_prod theorem

(x : M × M') : extChartAt (I.prod I') x = (extChartAt I x.1).prod (extChartAt I' x.2)

Full source

theorem extChartAt_prod (x : M × M') :
    extChartAt (I.prod I') x = (extChartAt I x.1).prod (extChartAt I' x.2) := by
  simp only [mfld_simps]
  -- Porting note: `simp` can't use `PartialEquiv.prod_trans` here because of a type
  -- synonym
  rw [PartialEquiv.prod_trans]

Product of Extended Charts Equals Extended Chart of Product

Informal description

For any point $x = (x_1, x_2)$ in the product manifold $M \times M'$ modeled on $(E \times E', H \times H')$, the extended chart at $x$ is equal to the product of the extended charts at $x_1$ in $M$ and $x_2$ in $M'$. More precisely, if $I$ and $I'$ are models with corners for $M$ and $M'$ respectively, then: \[ \text{extChartAt}_{I \times I'}(x_1, x_2) = \text{extChartAt}_I(x_1) \times \text{extChartAt}_{I'}(x_2) \] where the product of partial equivalences is defined componentwise.

extChartAt_comp theorem

 [ChartedSpace H H'] (x : M') :
  (letI := ChartedSpace.comp H H' M';
    extChartAt I x) =
    (chartAt H' x).toPartialEquiv ≫ extChartAt I (chartAt H' x x)

Full source

theorem extChartAt_comp [ChartedSpace H H'] (x : M') :
    (letI := ChartedSpace.comp H H' M'; extChartAt I x) =
      (chartAt H' x).toPartialEquiv ≫ extChartAt I (chartAt H' x x) :=
  PartialEquiv.trans_assoc ..

Composition of Extended Charts in a Charted Space

Informal description

Let $ M' $ be a manifold with a charted space structure over $ H' $, and let $ x \in M' $. The extended chart at $ x $ in the composition of charted spaces $ H $ and $ H' $ is equal to the composition of the chart at $ x $ (as a partial equivalence) with the extended chart at the image of $ x $ under the chart at $ x $. More precisely, under the composition charted space structure $ H \circ H' $, the extended chart $ \text{extChartAt}_I(x) $ is given by: \[ \text{extChartAt}_I(x) = \text{chartAt}_{H'}(x) \circ \text{extChartAt}_I(\text{chartAt}_{H'}(x)(x)) \] where $ \circ $ denotes the composition of partial equivalences.

writtenInExtChartAt_chartAt_comp theorem

 [ChartedSpace H H'] (x : M') {y}
  (hy :
    y ∈
      letI := ChartedSpace.comp H H' M';
      (extChartAt I x).target) :
  (letI := ChartedSpace.comp H H' M';
    writtenInExtChartAt I I x (chartAt H' x) y) =
    y

Full source

theorem writtenInExtChartAt_chartAt_comp [ChartedSpace H H'] (x : M') {y}
    (hy : y ∈ letI := ChartedSpace.comp H H' M'; (extChartAt I x).target) :
    (letI := ChartedSpace.comp H H' M'; writtenInExtChartAt I I x (chartAt H' x) y) = y := by
  letI := ChartedSpace.comp H H' M'
  simp_all only [mfld_simps, chartAt_comp]

Identity Property of Local Representation in Extended Charts

Informal description

Let $ M' $ be a manifold with a charted space structure over $ H' $, and let $ x \in M' $. For any point $ y $ in the target of the extended chart $ \text{extChartAt}_I(x) $ (under the composition charted space structure $ H \circ H' $), the local representation of the chart $ \text{chartAt}_{H'}(x) $ in the extended charts satisfies: \[ \text{writtenInExtChartAt}_I^I(x, \text{chartAt}_{H'}(x))(y) = y. \]

writtenInExtChartAt_chartAt_symm_comp theorem

 [ChartedSpace H H'] (x : M') {y}
  (hy :
    y ∈
      letI := ChartedSpace.comp H H' M';
      (extChartAt I x).target) :
  (letI := ChartedSpace.comp H H' M'
    writtenInExtChartAt I I (chartAt H' x x) (chartAt H' x).symm y) =
    y

Full source

theorem writtenInExtChartAt_chartAt_symm_comp [ChartedSpace H H'] (x : M') {y}
    (hy : y ∈ letI := ChartedSpace.comp H H' M'; (extChartAt I x).target) :
    ( letI := ChartedSpace.comp H H' M'
      writtenInExtChartAt I I (chartAt H' x x) (chartAt H' x).symm y) = y := by
  letI := ChartedSpace.comp H H' M'
  simp_all only [mfld_simps, chartAt_comp]

Local representation of inverse chart in extended charts is identity

Informal description

Let $ M' $ be a manifold with a charted space structure over $ H' $, and let $ x \in M' $. For any point $ y $ in the target of the extended chart $ \text{extChartAt}_I(x) $ (under the composition charted space structure $ H \circ H' $), the local representation of the inverse chart map $ \text{chartAt}_{H'}(x)^{-1} $ in the extended charts satisfies: \[ \text{writtenInExtChartAt}_I^I(\text{chartAt}_{H'}(x)(x), \text{chartAt}_{H'}(x)^{-1})(y) = y. \]

Manifold.locallyCompact_of_finiteDimensional theorem

(I : ModelWithCorners 𝕜 E H) [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E] : LocallyCompactSpace M

Full source

/-- A finite-dimensional manifold modelled on a locally compact field
(such as ℝ, ℂ or the `p`-adic numbers) is locally compact. -/
lemma Manifold.locallyCompact_of_finiteDimensional
    (I : ModelWithCorners 𝕜 E H) [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E] :
    LocallyCompactSpace M := by
  have : ProperSpace E := FiniteDimensional.proper 𝕜 E
  have : LocallyCompactSpace H := I.locallyCompactSpace
  exact ChartedSpace.locallyCompactSpace H M

Local compactness of finite-dimensional manifolds over locally compact fields

Informal description

Let $M$ be a smooth manifold modelled on a finite-dimensional vector space $E$ over a locally compact field $\mathbb{K}$ (such as $\mathbb{R}$, $\mathbb{C}$, or the $p$-adic numbers), with model space $H$ and model with corners $I : H \to E$. If $\mathbb{K}$ is locally compact and $E$ is finite-dimensional over $\mathbb{K}$, then $M$ is locally compact.

LocallyCompactSpace.of_locallyCompact_manifold theorem

(I : ModelWithCorners 𝕜 E H) [h : Nonempty M] [LocallyCompactSpace M] : LocallyCompactSpace E

Full source

/-- A locally compact manifold must be modelled on a locally compact space. -/
lemma LocallyCompactSpace.of_locallyCompact_manifold (I : ModelWithCorners 𝕜 E H)
    [h : Nonempty M] [LocallyCompactSpace M] :
    LocallyCompactSpace E := by
  rcases h with ⟨x⟩
  obtain ⟨y, hy⟩ := interior_extChartAt_target_nonempty I x
  have h'y : y ∈ (extChartAt I x).target := interior_subset hy
  obtain ⟨s, hmem, hss, hcom⟩ :=
    LocallyCompactSpace.local_compact_nhds ((extChartAt I x).symm y) (extChartAt I x).source
      ((isOpen_extChartAt_source x).mem_nhds ((extChartAt I x).map_target h'y))
  have : IsCompact <| (extChartAt I x) '' s :=
    hcom.image_of_continuousOn <| (continuousOn_extChartAt x).mono hss
  apply this.locallyCompactSpace_of_mem_nhds_of_addGroup (x := y)
  rw [← (extChartAt I x).right_inv h'y]
  apply extChartAt_image_nhd_mem_nhds_of_mem_interior_range
    (PartialEquiv.map_target (extChartAt I x) h'y) _ hmem
  simp only [(extChartAt I x).right_inv h'y]
  exact interior_mono (extChartAt_target_subset_range x) hy

Local Compactness of Model Space Implies Local Compactness of Manifold

Informal description

Let $M$ be a nonempty smooth manifold with corners modeled on $(E, H)$ with model with corners $I : H \to E$. If $M$ is locally compact, then the model vector space $E$ is also locally compact.

FiniteDimensional.of_locallyCompact_manifold theorem

[CompleteSpace 𝕜] (I : ModelWithCorners 𝕜 E H) [Nonempty M] [LocallyCompactSpace M] : FiniteDimensional 𝕜 E

Full source

/-- 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`. -/
theorem FiniteDimensional.of_locallyCompact_manifold
    [CompleteSpace 𝕜] (I : ModelWithCorners 𝕜 E H) [Nonempty M] [LocallyCompactSpace M] :
    FiniteDimensional 𝕜 E := by
  have := LocallyCompactSpace.of_locallyCompact_manifold M I
  exact FiniteDimensional.of_locallyCompactSpace 𝕜

Riesz's Theorem for Manifolds: Locally Compact Manifolds are Finite-Dimensional

Informal description

Let $M$ be a nonempty smooth manifold with corners modeled on $(E, H)$ with model with corners $I : H \to E$, where $\mathbb{K}$ is a complete normed field. If $M$ is locally compact, then the model vector space $E$ is finite-dimensional over $\mathbb{K}$.

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Main definitions

Main results