feat(Geometry/Manifold): interior and boundary of open subsets of manifolds (leanprover-community#32759)

A belongs to the interior / boundary of an open submanifold iff it belongs to the interior / boundary, when regarded as a point of the ambient manifold.

Author: peabrainiac

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -1311,6 +1311,8 @@ protected instance instChartedSpace : ChartedSpace H s where
     simp only [mem_iUnion, mem_singleton_iff]
     use x
 
+lemma chartAt_eq {s : Opens M} {x : s} : chartAt H x = (chartAt H x.1).subtypeRestr ⟨x⟩ := rfl
+
 /-- If `s` is a non-empty open subset of `M`, every chart of `s` is the restriction
 of some chart on `M`. -/
 lemma chart_eq {s : Opens M} (hs : Nonempty s) {e : OpenPartialHomeomorph s H}

Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean

@@ -24,6 +24,13 @@ Define the interior and boundary of a manifold.
 - `BoundarylessManifold.isInteriorPoint`: if `M` is boundaryless, every point is an interior point
 - `ModelWithCorners.Boundaryless.boundary_eq_empty` and `of_boundary_eq_empty`:
 `M` is boundaryless if and only if its boundary is empty
+
+- `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
+  of `M` under the inclusion
+- `ModelWithCorners.BoundarylessManifold.open`: if `M` is boundaryless, so is `u : Opens M`
+
 - `ModelWithCorners.interior_prod`: the interior of `M × N` is the product of the interiors
 of `M` and `N`.
 - `ModelWithCorners.boundary_prod`: the boundary of `M × N` is `∂M × N ∪ (M × ∂N)`.
@@ -190,6 +197,39 @@ lemma Boundaryless.of_boundary_eq_empty (h : I.boundary M = ∅) : BoundarylessM
 
 end BoundarylessManifold
 
+/-! Interior and boundary of open subsets of a manifold. -/
+section opens
+
+open TopologicalSpace
+
+/-- For `u : Opens M`, `x : u` is an interior point iff `x.val : M` is. -/
+lemma isInteriorPoint_iff_isInteriorPoint_val {u : Opens M} {x : u} :
+    I.IsInteriorPoint x ↔ I.IsInteriorPoint x.1 := by
+  simpa [I.isInteriorPoint_iff, u.chartAt_eq,
+    OpenPartialHomeomorph.subtypeRestr, mem_interior_iff_mem_nhds] using
+    fun _ _ ↦ (chartAt H x.1).extend_preimage_mem_nhds (mem_chart_source H x.1) (u.2.mem_nhds x.2)
+
+/-- For `u : Opens M`, `x : u` is a boundary point iff `x.val : M` is. -/
+lemma isBoundaryPoint_iff_isBoundaryPoint_val {u : Opens M} {x : u} :
+    I.IsBoundaryPoint x ↔ I.IsBoundaryPoint x.1 := by
+  simpa [I.isInteriorPoint_iff_not_isBoundaryPoint, not_iff_not] using
+    I.isInteriorPoint_iff_isInteriorPoint_val
+
+/-- The interior of `u : Opens M` is the preimage of the interior of `M` under the inclusion. -/
+lemma interior_open {u : Opens M} : I.interior u = (↑) ⁻¹' I.interior M := by
+  ext1; exact I.isInteriorPoint_iff_isInteriorPoint_val
+
+/-- The boundary of `u : Opens M` is the preimage of the boundary of `M` under the inclusion. -/
+lemma boundary_open {u : Opens M} : I.boundary u = (↑) ⁻¹' I.boundary M := by
+  simp [← I.compl_interior, I.interior_open]
+
+/-- Open subsets of boundaryless manifolds are boundaryless. -/
+instance BoundarylessManifold.open [BoundarylessManifold I M] (u : Opens M) :
+    BoundarylessManifold I u :=
+  ⟨fun _ ↦ I.isInteriorPoint_iff_isInteriorPoint_val.2 BoundarylessManifold.isInteriorPoint⟩
+
+end opens
+
 /-! Interior and boundary of the product of two manifolds. -/
 section prod
 
@@ -250,11 +290,11 @@ instance BoundarylessManifold.prod [BoundarylessManifold I M] [BoundarylessManif
 
 end prod
 
+/-! Interior and boundary of the disjoint union of two manifolds. -/
 section disjointUnion
 
 variable {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞}
   {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
-  {J : Type*} {J : ModelWithCorners 𝕜 E' H'}
   {N N' : Type*} [TopologicalSpace N] [TopologicalSpace N'] [ChartedSpace H' N] [ChartedSpace H' N']
 
 open Topology