Skip to content

Commit ae8f621

Browse files
committed
feat: four small lemmas about extended charts (#10001)
From sphere-eversion; I'm just submitting them.
1 parent c8818ba commit ae8f621

File tree

1 file changed

+19
-0
lines changed

1 file changed

+19
-0
lines changed

Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1025,12 +1025,21 @@ theorem map_extend_nhds {x : M} (hy : x ∈ f.source) :
10251025
rwa [extend_coe, comp_apply, ← I.map_nhds_eq, ← f.map_nhds_eq, map_map]
10261026
#align local_homeomorph.map_extend_nhds PartialHomeomorph.map_extend_nhds
10271027

1028+
theorem map_extend_nhds_of_boundaryless [I.Boundaryless] {x : M} (hx : x ∈ f.source) :
1029+
map (f.extend I) (𝓝 x) = 𝓝 (f.extend I x) := by
1030+
rw [f.map_extend_nhds _ hx, I.range_eq_univ, nhdsWithin_univ]
1031+
10281032
theorem extend_target_mem_nhdsWithin {y : M} (hy : y ∈ f.source) :
10291033
(f.extend I).target ∈ 𝓝[range I] f.extend I y := by
10301034
rw [← PartialEquiv.image_source_eq_target, ← map_extend_nhds f I hy]
10311035
exact image_mem_map (extend_source_mem_nhds _ _ hy)
10321036
#align local_homeomorph.extend_target_mem_nhds_within PartialHomeomorph.extend_target_mem_nhdsWithin
10331037

1038+
theorem extend_image_nhd_mem_nhds_of_boundaryless [I.Boundaryless] {x} (hx : x ∈ f.source)
1039+
{s : Set M} (h : s ∈ 𝓝 x) : (f.extend I) '' s ∈ 𝓝 ((f.extend I) x) := by
1040+
rw [← f.map_extend_nhds_of_boundaryless _ hx, Filter.mem_map]
1041+
filter_upwards [h] using subset_preimage_image (f.extend I) s
1042+
10341043
theorem extend_target_subset_range : (f.extend I).target ⊆ range I := by simp only [mfld_simps]
10351044
#align local_homeomorph.extend_target_subset_range PartialHomeomorph.extend_target_subset_range
10361045

@@ -1356,6 +1365,16 @@ theorem map_extChartAt_nhds : map (extChartAt I x) (𝓝 x) = 𝓝[range I] extC
13561365
map_extChartAt_nhds' I <| mem_extChartAt_source I x
13571366
#align map_ext_chart_at_nhds map_extChartAt_nhds
13581367

1368+
theorem map_extChartAt_nhds_of_boundaryless [I.Boundaryless] :
1369+
map (extChartAt I x) (𝓝 x) = 𝓝 (extChartAt I x x) := by
1370+
rw [extChartAt]
1371+
exact map_extend_nhds_of_boundaryless (chartAt H x) I (mem_chart_source H x)
1372+
1373+
theorem extChartAt_image_nhd_mem_nhds_of_boundaryless [I.Boundaryless]
1374+
(h : s ∈ 𝓝 x) : extChartAt I x '' s ∈ 𝓝 (extChartAt I x x) := by
1375+
rw [extChartAt]
1376+
exact extend_image_nhd_mem_nhds_of_boundaryless _ I (mem_chart_source H x) h
1377+
13591378
theorem extChartAt_target_mem_nhdsWithin' {y : M} (hy : y ∈ (extChartAt I x).source) :
13601379
(extChartAt I x).target ∈ 𝓝[range I] extChartAt I x y :=
13611380
extend_target_mem_nhdsWithin _ _ <| by rwa [← extChartAt_source I]

0 commit comments

Comments
 (0)