diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index cc31a4c1053e2d..ebb77cc902a307 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -370,6 +370,61 @@ theorem contDiffWithinAt_extend_coord_change' [ChartedSpace H M] (hf : f ∈ max end OpenPartialHomeomorph +namespace ModelWithCorners + +/-- The change of charts from `e` to `e'` in the model vector space `E`. -/ +@[simps!] +def extCoordChange (e e' : OpenPartialHomeomorph M H) : PartialEquiv E E := + (e.extend I).symm.trans (e'.extend I) + +variable {e e' : OpenPartialHomeomorph M H} + +lemma extCoordChange_symm : (I.extCoordChange e e').symm = I.extCoordChange e' e := by + rfl + +lemma uniqueDiffOn_extCoordChange_source : UniqueDiffOn 𝕜 (I.extCoordChange e e').source := by + rw [extCoordChange_source, inter_assoc, inter_comm, preimage_comp, ← preimage_inter] + exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source + +lemma uniqueDiffOn_extCoordChange_target : UniqueDiffOn 𝕜 (I.extCoordChange e e').target := by + rw [← extCoordChange_symm, PartialEquiv.symm_target] + exact uniqueDiffOn_extCoordChange_source + +variable [ChartedSpace H M] {n : WithTop ℕ∞} + +lemma contDiffOn_extCoordChange (he : e ∈ IsManifold.maximalAtlas I n M) + (he' : e' ∈ IsManifold.maximalAtlas I n M) : + ContDiffOn 𝕜 n (I.extCoordChange e e') (I.extCoordChange e e').source := + e'.contDiffOn_extend_coord_change he' he + +lemma contDiffOn_extCoordChange_symm (he : e ∈ IsManifold.maximalAtlas I n M) + (he' : e' ∈ IsManifold.maximalAtlas I n M) : + ContDiffOn 𝕜 n (I.extCoordChange e e').symm (I.extCoordChange e e').target := + e.contDiffOn_extend_coord_change he he' + +lemma isInvertible_fderivWithin_extCoordChange (hn : n ≠ 0) (he : e ∈ IsManifold.maximalAtlas I n M) + (he' : e' ∈ IsManifold.maximalAtlas I n M) {x : E} (hx : x ∈ (I.extCoordChange e e').source) : + (fderivWithin 𝕜 (I.extCoordChange e e') (I.extCoordChange e e').source x).IsInvertible := by + set φ := I.extCoordChange e e' + have hφ : ContDiffOn 𝕜 n φ φ.source := I.contDiffOn_extCoordChange he he' + have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := I.contDiffOn_extCoordChange_symm he he' + refine .of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_ + · rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp, + fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx), fderivWithin_id] + · exact I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx) + · exact (φ.left_inv hx ▸ ((hφ _ hx).differentiableWithinAt hn):) + · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn + · exact φ.symm_mapsTo + · exact I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx) + · rw [← fderivWithin_comp, fderivWithin_congr' φ.leftInvOn.eqOn hx, fderivWithin_id] + · exact I.uniqueDiffOn_extCoordChange_source _ hx + · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn + · exact (hφ _ hx).differentiableWithinAt hn + · exact φ.mapsTo + · exact I.uniqueDiffOn_extCoordChange_source _ hx + +end ModelWithCorners + open OpenPartialHomeomorph variable [ChartedSpace H M] [ChartedSpace H' M'] @@ -743,6 +798,13 @@ theorem writtenInExtChartAt_extChartAt_symm {x : M} {y : E} (h : y ∈ (extChart writtenInExtChartAt 𝓘(𝕜, E) I (extChartAt I x x) (extChartAt I x).symm y = y := by simp_all only [mfld_simps] +theorem writtenInExtChartAt_mapsTo {x : M} {f : M → M'} : + MapsTo (writtenInExtChartAt I I' x f) + ((extChartAt I x).target ∩ f ∘ (extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source) + (extChartAt I' (f x)).target := by + intro x' hx' + simpa using (chartAt H' (f x)).mapsTo (by simpa using hx'.2) + section variable {G G' F F' N N' : Type*} diff --git a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean index 791ab7b7cbcfd7..08b17d10a5dd0f 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean @@ -1,11 +1,14 @@ /- Copyright (c) 2023 Michael Rothgang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Michael Rothgang +Authors: Michael Rothgang, Ben Eltschig -/ module -public import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt +public import Mathlib.Geometry.Manifold.LocalDiffeomorph + +import Mathlib.Analysis.Calculus.LocalExtr.Basic +import Mathlib.Analysis.LocallyConvex.Separation /-! # Interior and boundary of a manifold @@ -25,6 +28,9 @@ Define the interior and boundary of a manifold. - `ModelWithCorners.Boundaryless.boundary_eq_empty` and `of_boundary_eq_empty`: `M` is boundaryless if and only if its boundary is empty +- `ModelWithCorners.isOpen_interior`, `ModelWithCorners.isClosed_boundary`: the interior is open and + and the boundary is closed. This is currently only proven for C¹ manifolds. + - `ModelWithCorners.interior_open`: the interior of `u : Opens M` is the preimage of the interior of `M` under the inclusion - `ModelWithCorners.boundary_open`: the boundary of `u : Opens M` is the preimage of the boundary @@ -47,22 +53,23 @@ of `M` and `N`. manifold, interior, boundary ## TODO -- `x` is an interior point iff *any* chart around `x` maps it to `interior (range I)`; -similarly for the boundary. -- the interior of `M` is open, hence the boundary is closed (and nowhere dense) - In finite dimensions, this requires e.g. the homology of spheres. -- the interior of `M` is a manifold without boundary +- the interior of `M` is dense, the boundary nowhere dense +- the interior of `M` is a boundaryless manifold - `boundary M` is a submanifold (possibly with boundary and corners): -follows from the corresponding statement for the model with corners `I`; -this requires a definition of submanifolds + follows from the corresponding statement for the model with corners `I`; + this requires a definition of submanifolds - if `M` is finite-dimensional, its boundary has measure zero +- generalise lemmas about C¹ manifolds with boundary to also hold for finite-dimensional topological + manifolds; this will require e.g. the homology of spheres. +- submersions send interior points to interior points. This should be an easy consequence of + `MDifferentiableAt.isInteriorPoint_of_surjective_mfderiv` once submersions are defined. -/ @[expose] public section -open Set -open scoped Topology +open Set Function +open scoped Topology Manifold -- Let `M` be a manifold with corners over the pair `(E, H)`. variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] @@ -73,12 +80,12 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] namespace ModelWithCorners variable (I) in -/-- `p ∈ M` is an interior point of a manifold `M` iff its image in the extended chart +/-- `p ∈ M` is an interior point of a manifold `M` if and only if its image in the extended chart lies in the interior of the model space. -/ def IsInteriorPoint (x : M) := extChartAt I x x ∈ interior (range I) variable (I) in -/-- `p ∈ M` is a boundary point of a manifold `M` iff its image in the extended chart +/-- `p ∈ M` is a boundary point of a manifold `M` if and only if its image in the extended chart lies on the boundary of the model space. -/ def IsBoundaryPoint (x : M) := extChartAt I x x ∈ frontier (range I) @@ -126,6 +133,10 @@ lemma isInteriorPoint_iff_not_isBoundaryPoint (x : M) : ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff] exact h +lemma isBoundaryPoint_iff_not_isInteriorPoint (x : M) : + I.IsBoundaryPoint x ↔ ¬I.IsInteriorPoint x := by + simp [isInteriorPoint_iff_not_isBoundaryPoint] + /-- The boundary is the complement of the interior. -/ lemma compl_interior : (I.interior M)ᶜ = I.boundary M := by apply compl_unique ?_ I.interior_union_boundary_eq_univ @@ -182,7 +193,7 @@ lemma Boundaryless.boundary_eq_empty [BoundarylessManifold I M] : I.boundary M = instance [BoundarylessManifold I M] : IsEmpty (I.boundary M) := isEmpty_coe_sort.mpr Boundaryless.boundary_eq_empty -/-- `M` is boundaryless iff its boundary is empty. -/ +/-- `M` is boundaryless if and only if its boundary is empty. -/ lemma Boundaryless.iff_boundary_eq_empty : I.boundary M = ∅ ↔ BoundarylessManifold I M := by refine ⟨fun h ↦ { isInteriorPoint' := ?_ }, fun a ↦ boundary_eq_empty⟩ intro x @@ -197,6 +208,215 @@ lemma Boundaryless.of_boundary_eq_empty (h : I.boundary M = ∅) : BoundarylessM end BoundarylessManifold +section ChartIndependence + +/-- If a function `f : E → H` is differentiable at `x`, sends a neighbourhood `u` of `x` to a +closed convex set `s` with nonempty interior and has surjective differential at `x`, it must send +`x` to the interior of `s`. +TODO: find home (`#find_home` says this file) -/ +lemma _root_.DifferentiableAt.mem_interior_convex_of_surjective_fderiv {E H : Type*} + [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup H] [NormedSpace ℝ H] {f : E → H} + {x : E} (hf : DifferentiableAt ℝ f x) {u : Set E} (hu : u ∈ 𝓝 x) {s : Set H} (hs : Convex ℝ s) + (hs' : IsClosed s) (hs'' : (interior s).Nonempty) (hfus : Set.MapsTo f u s) + (hfx : Function.Surjective (fderiv ℝ f x)) : f x ∈ interior s := by + contrapose hfx + have ⟨F, hF⟩ := geometric_hahn_banach_open_point hs.interior isOpen_interior hfx + -- It suffices to show that `fderiv ℝ f x` sends everything to the kernel of `F`. + suffices h : ∀ y, F (fderiv ℝ f x y) = 0 by + have ⟨y, hy⟩ := hs'' + unfold Function.Surjective; push_neg + refine ⟨f x - y, fun z ↦ ne_of_apply_ne F ?_⟩ + rw [h z, F.map_sub] + exact (sub_pos.2 <| hF _ hy).ne + -- This follows from `F ∘ f` taking on a local maximum at `e.extend I x`. + have hF' : MapsTo F s (Iic (F (f x))) := by + rw [← hs'.closure_eq, ← closure_Iio, ← hs.closure_interior_eq_closure_of_nonempty_interior hs''] + exact .closure hF F.continuous + have hFφ : IsLocalMax (F ∘ f) x := Filter.eventually_of_mem hu fun y hy ↦ hF' <| hfus hy + have h := hFφ.fderiv_eq_zero + rw [fderiv_comp _ (by fun_prop) hf, ContinuousLinearMap.fderiv] at h + exact DFunLike.congr_fun h + +/-- A point `x` in a C¹ manifold is an interior point if and only if it gets mapped to the interior +of the model space by any given chart - in other words, the notion of interior points does not +depend on any choice of charts. + +Note that in general, this is actually quite nontrivial; that is why are focusing only on C¹ +manifolds here. For merely topological finite-dimensional manifolds the proof involves singular +homology, and for infinite-dimensional topological manifolds I don't even know if this lemma holds. +-/ +lemma isInteriorPoint_iff_of_mem_atlas {n : WithTop ℕ∞} [IsManifold I n M] (hn : n ≠ 0) + {e : OpenPartialHomeomorph M H} (he : e ∈ atlas H M) {x : M} (hx : x ∈ e.source) : + I.IsInteriorPoint x ↔ e.extend I x ∈ interior (e.extend I).target := by + -- it suffices to show that if `x` is interior in one chart `e` it also is in any other chart `e'` + revert e + suffices h : ∀ e ∈ atlas H M, x ∈ e.source → ∀ e' ∈ atlas H M, x ∈ e'.source → + e.extend I x ∈ interior (e.extend I).target → e'.extend I x ∈ interior (e'.extend I).target by + rw [isInteriorPoint_iff] + exact fun e he hx ↦ ⟨h _ (chart_mem_atlas H x) (mem_chart_source H x) _ he hx, + h _ he hx _ (chart_mem_atlas H x) (mem_chart_source H x)⟩ + intro e he hex e' he' hex' hx + /- Since transition maps are diffeomorphisms, it suffices to show that if `e'` were to send `x` + to the boundary of `range I`, the differential of the transition map `φ` from `e` to `e'` at `x` + could not be surjective. -/ + let φ := (e.extend I).symm.trans (e'.extend I) + have hφ : ContDiffOn 𝕜 n φ φ.source := e'.contDiffOn_extend_coord_change + (IsManifold.subset_maximalAtlas he') (IsManifold.subset_maximalAtlas he) + suffices h : Function.Surjective (fderivWithin 𝕜 φ φ.source (e.extend I x)) → + e'.extend I x ∈ interior (range I) by + refine e'.mem_interior_extend_target (by simp [hex']) <| h ?_ + exact (isInvertible_fderivWithin_extCoordChange hn (IsManifold.subset_maximalAtlas he) + (IsManifold.subset_maximalAtlas he') <| by simp [hex, hex']).surjective + intro hφx' + /- Reduce the situation to the real case, then apply + `DifferentiableAt.mem_interior_convex_of_surjective_fderiv`. -/ + wlog _ : IsRCLikeNormedField 𝕜 + · simp [I.range_eq_univ_of_not_isRCLikeNormedField ‹_›] + let _ := IsRCLikeNormedField.rclike 𝕜 + let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E + have hφx : φ.source ∈ 𝓝 (e.extend I x) := by + simp_rw [φ, PartialEquiv.trans_source, PartialEquiv.symm_source, Filter.inter_mem_iff, + mem_interior_iff_mem_nhds.1 hx, true_and, e'.extend_source] + exact e.extend_preimage_mem_nhds hex <| e'.open_source.mem_nhds hex' + rw [← ContinuousLinearMap.coe_restrictScalars' (R := ℝ), + (hφ.differentiableOn hn _ (by simp [φ, hex, hex'])).restrictScalars_fderivWithin (𝕜 := ℝ) + (uniqueDiffWithinAt_of_mem_nhds hφx), fderivWithin_of_mem_nhds <| hφx] at hφx' + rw [show e'.extend I x = φ (e.extend I x) by simp [φ, hex]] + replace hφ := ((hφ.restrict_scalars ℝ).differentiableOn hn).differentiableAt hφx + exact hφ.mem_interior_convex_of_surjective_fderiv hφx I.convex_range I.isClosed_range + I.nonempty_interior (φ.mapsTo.mono_right <| by simp [φ, inter_assoc]) hφx' + +/-- A point `x` in a C¹ manifold is a boundary point if and only if it gets mapped to the boundary +of the model space by any given chart - in other words, the notion of boundary points does not +depend on any choice of charts. + +Also see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`. -/ +lemma isBoundaryPoint_iff_of_mem_atlas {n : WithTop ℕ∞} [IsManifold I n M] (hn : n ≠ 0) + {e : OpenPartialHomeomorph M H} (he : e ∈ atlas H M) {x : M} (hx : x ∈ e.source) : + I.IsBoundaryPoint x ↔ e.extend I x ∈ frontier (e.extend I).target := by + rw [← not_iff_not, ← I.isInteriorPoint_iff_not_isBoundaryPoint, + I.isInteriorPoint_iff_of_mem_atlas hn he hx, mem_interior_iff_notMem_frontier] + exact (e.extend I).mapsTo <| e.extend_source (I := I) ▸ hx + +/-- The interior of any C¹ manifold is open. + +This is currently only proven for C¹ manifolds, but holds at least for finite-dimensional +topological manifolds too; see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`. -/ +protected lemma isOpen_interior {n : WithTop ℕ∞} [IsManifold I n M] (hn : n ≠ 0) : + IsOpen (I.interior M) := by + refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ⟨_, ?_, isOpen_extChartAt_preimage (I := I) x + isOpen_interior, mem_chart_source H x, isInteriorPoint_iff.1 hx⟩ + exact fun y hy ↦ (I.isInteriorPoint_iff_of_mem_atlas hn (chart_mem_atlas H x) hy.1).2 hy.2 + +/-- The boundary of any C¹ manifold is closed. + +This is currently only proven for C¹ manifolds, but holds at least for finite-dimensional +topological manifolds too; see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`. -/ +protected lemma isClosed_boundary {n : WithTop ℕ∞} [IsManifold I n M] (hn : n ≠ 0) : + IsClosed (I.boundary M) := by + rw [← I.compl_interior, isClosed_compl_iff] + exact I.isOpen_interior hn + +end ChartIndependence + +/-! Interior and boundary are preserved under (local) diffeomorphisms. -/ +section Diffeomorph + +variable + {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] + {H' : Type*} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} + {N : Type*} [TopologicalSpace N] [ChartedSpace H' N] + {n : WithTop ℕ∞} + +/-- If a function `f` is differentiable at `x` with surjective `mfderiv I I' f x` and `x` is an +interior point with respect to `I`, `f x` must be an interior point with respect to `I'`. -/ +lemma _root_.MDifferentiableAt.isInteriorPoint_of_surjective_mfderiv {f : M → N} {x : M} + (hf : MDifferentiableAt I I' f x) (hf' : Surjective (mfderiv I I' f x)) + (hx : I.IsInteriorPoint x) : I'.IsInteriorPoint (f x) := by + wlog _ : IsRCLikeNormedField 𝕜 + · simp [IsInteriorPoint, I'.range_eq_univ_of_not_isRCLikeNormedField ‹_›] + let _ := IsRCLikeNormedField.rclike 𝕜 + let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E + let _ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E' + simp only [mfderiv, hf, ite_true] at hf' + have hf'' := hf.differentiableWithinAt_writtenInExtChartAt.differentiableAt <| by + simpa [← mem_interior_iff_mem_nhds] using hx + rw [fderivWithin_eq_fderiv (I.uniqueDiffOn _ <| by simp) hf''] at hf' + replace hf' : Surjective (fderiv ℝ (writtenInExtChartAt I I' x f) (extChartAt I x x)) := by + rwa [hf''.fderiv_restrictScalars (𝕜 := ℝ), ContinuousLinearMap.coe_restrictScalars'] + replace hf'' := hf''.restrictScalars ℝ + have := hf''.mem_interior_convex_of_surjective_fderiv (Filter.inter_mem ?_ ?_) I'.convex_range + I'.isClosed_range I'.nonempty_interior (writtenInExtChartAt_mapsTo.mono_right ?_) hf' + · simpa using this + · rw [← nhdsWithin_eq_nhds.2 (mem_interior_iff_mem_nhds.1 hx)] + exact extChartAt_target_mem_nhdsWithin x + · exact extChartAt_preimage_mem_nhds <| hf.continuousAt.preimage_mem_nhds <| + extChartAt_source_mem_nhds _ + · exact extChartAt_target_subset_range _ + +lemma _root_.IsLocalDiffeomorphAt.isInteriorPoint_iff (hn : n ≠ 0) {f : M → N} {x : M} + (hf : IsLocalDiffeomorphAt I I' n f x) : I.IsInteriorPoint x ↔ I'.IsInteriorPoint (f x) := by + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + · refine (hf.mdifferentiableAt hn).isInteriorPoint_of_surjective_mfderiv ?_ h + exact (hf.mfderivToContinuousLinearEquiv hn).surjective + · rw [← hf.localInverse_left_inv hf.localInverse_mem_target] + refine (hf.localInverse_mdifferentiableAt hn).isInteriorPoint_of_surjective_mfderiv ?_ h + exact (hf.mfderivToContinuousLinearEquiv hn).symm.surjective + +lemma _root_.IsLocalDiffeomorphAt.isBoundaryPoint_iff (hn : n ≠ 0) {f : M → N} {x : M} + (hf : IsLocalDiffeomorphAt I I' n f x) : I.IsBoundaryPoint x ↔ I'.IsBoundaryPoint (f x) := by + simp [isBoundaryPoint_iff_not_isInteriorPoint, hf.isInteriorPoint_iff hn] + + +lemma _root_.IsLocalDiffeomorphOn.preimage_interior_inter (hn : n ≠ 0) {f : M → N} {s : Set M} + (hf : IsLocalDiffeomorphOn I I' n f s) : f ⁻¹' I'.interior N ∩ s = I.interior M ∩ s := by + ext x + simpa using fun hx ↦ ((hf ⟨x, hx⟩).isInteriorPoint_iff hn).symm + +lemma _root_.IsLocalDiffeomorphOn.preimage_boundary_inter (hn : n ≠ 0) {f : M → N} {s : Set M} + (hf : IsLocalDiffeomorphOn I I' n f s) : f ⁻¹' I'.boundary N ∩ s = I.boundary M ∩ s := by + ext x + simpa using fun hx ↦ ((hf ⟨x, hx⟩).isBoundaryPoint_iff hn).symm + +lemma _root_.IsLocalDiffeomorph.preimage_interior (hn : n ≠ 0) {f : M → N} + (hf : IsLocalDiffeomorph I I' n f) : f ⁻¹' I'.interior N = I.interior M := by + simpa using (hf.isLocalDiffeomorphOn univ).preimage_interior_inter hn + +lemma _root_.IsLocalDiffeomorph.preimage_boundary (hn : n ≠ 0) {f : M → N} + (hf : IsLocalDiffeomorph I I' n f) : f ⁻¹' I'.boundary N = I.boundary M := by + simpa using (hf.isLocalDiffeomorphOn univ).preimage_boundary_inter hn + +lemma _root_.IsLocalDiffeomorph.boundarylessManifold (hn : n ≠ 0) {f : M → N} + (hf : IsLocalDiffeomorph I I' n f) [BoundarylessManifold I' N] : BoundarylessManifold I M := by + simp [← Boundaryless.iff_boundary_eq_empty, ← hf.preimage_boundary hn, + Boundaryless.boundary_eq_empty] + +lemma _root_.Diffeomorph.preimage_interior (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) : + Φ ⁻¹' I'.interior N = I.interior M := + Φ.isLocalDiffeomorph.preimage_interior hn + +lemma _root_.Diffeomorph.preimage_boundary (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) : + Φ ⁻¹' I'.boundary N = I.boundary M := + Φ.isLocalDiffeomorph.preimage_boundary hn + +lemma _root_.Diffeomorph.image_interior (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) : + Φ '' I.interior M = I'.interior N := + (Φ.eq_preimage_iff_image_eq _ _).1 (Φ.preimage_interior hn).symm + +lemma _root_.Diffeomorph.image_boundary (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) : + Φ '' I.boundary M = I'.boundary N := + (Φ.eq_preimage_iff_image_eq _ _).1 (Φ.preimage_boundary hn).symm + +lemma _root_.Diffeomorph.boundarylessManifold (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) + [BoundarylessManifold I M] : BoundarylessManifold I' N := + Φ.symm.isLocalDiffeomorph.boundarylessManifold hn + +lemma _root_.Diffeomorph.boundarylessManifold_iff (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) : + BoundarylessManifold I M ↔ BoundarylessManifold I' N := + ⟨fun _ ↦ Φ.boundarylessManifold hn, fun _ ↦ Φ.symm.boundarylessManifold hn⟩ + +end Diffeomorph + /-! Interior and boundary of open subsets of a manifold. -/ section opens @@ -294,8 +514,6 @@ end prod section disjointUnion variable {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} - {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] - {N N' : Type*} [TopologicalSpace N] [TopologicalSpace N'] [ChartedSpace H' N] [ChartedSpace H' N'] open Topology diff --git a/Mathlib/Topology/Closure.lean b/Mathlib/Topology/Closure.lean index 9fce1bcde43b43..2c498c2afa91c4 100644 --- a/Mathlib/Topology/Closure.lean +++ b/Mathlib/Topology/Closure.lean @@ -489,6 +489,14 @@ theorem self_diff_frontier (s : Set X) : s \ frontier s = interior s := by rw [frontier, diff_diff_right, diff_eq_empty.2 subset_closure, inter_eq_self_of_subset_right interior_subset, empty_union] +lemma mem_interior_iff_notMem_frontier {s : Set X} {x : X} (hx : x ∈ s) : + x ∈ interior s ↔ x ∉ frontier s := by + simp [← self_diff_frontier, hx] + +lemma mem_frontier_iff_notMem_interior {s : Set X} {x : X} (hx : x ∈ s) : + x ∈ frontier s ↔ x ∉ interior s := by + simp [← self_diff_frontier, hx] + theorem frontier_eq_closure_inter_closure : frontier s = closure s ∩ closure sᶜ := by rw [closure_compl, frontier, diff_eq]