cherry pick

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -705,6 +705,18 @@ theorem chartAt_comp (H : Type*) [TopologicalSpace H] (H' : Type*) [TopologicalS
     (letI := ChartedSpace.comp H H' M; chartAt H x) = chartAt H' x ≫ₕ chartAt H (chartAt H' x x) :=
   rfl
 
+/-- A charted space over a T1 space is T1. Note that this is *not* true for T2. -/
+theorem ChartedSpace.t1Space [T1Space H] : T1Space M := by
+  apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)
+  by_cases hy : y ∈ (chartAt H x).source
+  · refine ⟨(chartAt H x).source ∩ (chartAt H x)⁻¹' ({chartAt H x y}ᶜ), ?_, ?_, ?_⟩
+    · exact PartialHomeomorph.isOpen_inter_preimage _ isOpen_compl_singleton
+    · simp only [preimage_compl, mem_inter_iff, mem_chart_source, mem_compl_iff, mem_preimage,
+        mem_singleton_iff, true_and]
+      exact (chartAt H x).injOn.ne (ChartedSpace.mem_chart_source x) hy hxy
+    · simp
+  · exact ⟨(chartAt H x).source, (chartAt H x).open_source, ChartedSpace.mem_chart_source x, hy⟩
+
 end
 
 library_note "Manifold type tags" /-- For technical reasons we introduce two type tags:

Mathlib/Geometry/Manifold/Diffeomorph.lean

@@ -446,6 +446,15 @@ def transDiffeomorph (I : ModelWithCorners 𝕜 E H) (e : E ≃ₘ[𝕜] E') : M
   toPartialEquiv := I.toPartialEquiv.trans e.toEquiv.toPartialEquiv
   source_eq := by simp
   uniqueDiffOn' := by simp [range_comp e, I.uniqueDiffOn]
+  target_subset_closure_interior := by
+    simp only [PartialEquiv.trans_target, Equiv.toPartialEquiv_target,
+      Equiv.toPartialEquiv_symm_apply, Diffeomorph.toEquiv_coe_symm, target_eq, univ_inter]
+    change e.toHomeomorph.symm ⁻¹' _ ⊆ closure (interior (e.toHomeomorph.symm ⁻¹' (range I)))
+    rw [← IsOpenMap.preimage_interior_eq_interior_preimage e.toHomeomorph.symm.isOpenMap
+      e.toHomeomorph.continuous_symm,
+      ← IsOpenMap.preimage_closure_eq_closure_preimage e.toHomeomorph.symm.isOpenMap
+      e.toHomeomorph.continuous_symm]
+    exact preimage_mono I.range_subset_closure_interior
   continuous_toFun := e.continuous.comp I.continuous
   continuous_invFun := I.continuous_symm.comp e.symm.continuous
 

Mathlib/Geometry/Manifold/Instances/Real.lean

@@ -104,6 +104,13 @@ theorem closure_halfspace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
   let f : PiLp p (fun _ : Fin n ↦ ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
   simpa [closure_Ici] using f.closure_preimage (Function.surjective_eval _) (Ici a)
 
+open ENNReal in
+@[simp]
+theorem closure_open_halfspace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
+    closure { y : PiLp p (fun _ : Fin n ↦ ℝ) | a < y i } = { y | a ≤ y i } := by
+  let f : PiLp p (fun _ : Fin n ↦ ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
+  simpa [closure_Ioi] using f.closure_preimage (Function.surjective_eval _) (Ioi a)
+
 open ENNReal in
 @[simp]
 theorem frontier_halfspace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
@@ -141,6 +148,7 @@ def modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] :
       UniqueDiffOn.pi (Fin n) (fun _ => ℝ) _ _ fun i (_ : i ∈ ({0} : Set (Fin n))) =>
         uniqueDiffOn_Ici 0
     simpa only [singleton_pi] using this
+  target_subset_closure_interior := by simp
   continuous_toFun := continuous_subtype_val
   continuous_invFun := by
     exact (continuous_id.update 0 <| (continuous_apply 0).max continuous_const).subtype_mk _
@@ -163,6 +171,12 @@ def modelWithCornersEuclideanQuadrant (n : ℕ) :
     have this : UniqueDiffOn ℝ _ :=
       UniqueDiffOn.univ_pi (Fin n) (fun _ => ℝ) _ fun _ => uniqueDiffOn_Ici 0
     simpa only [pi_univ_Ici] using this
+  target_subset_closure_interior := by
+    have : {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x i}
+      = Set.pi univ (fun i ↦ Ici 0) := by aesop
+    simp only [this, interior_pi_set finite_univ]
+    rw [closure_pi_set]
+    simp
   continuous_toFun := continuous_subtype_val
   continuous_invFun := Continuous.subtype_mk
     (continuous_pi fun i => (continuous_id.max continuous_const).comp (continuous_apply i)) _

Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

@@ -149,6 +149,7 @@ structure ModelWithCorners (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Ty
     PartialEquiv H E where
   source_eq : source = univ
   uniqueDiffOn' : UniqueDiffOn 𝕜 toPartialEquiv.target
+  target_subset_closure_interior : toPartialEquiv.target ⊆ closure (interior toPartialEquiv.target)
   continuous_toFun : Continuous toFun := by continuity
   continuous_invFun : Continuous invFun := by continuity
 
@@ -160,6 +161,7 @@ def modelWithCornersSelf (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type
   toPartialEquiv := PartialEquiv.refl E
   source_eq := rfl
   uniqueDiffOn' := uniqueDiffOn_univ
+  target_subset_closure_interior := by simp
   continuous_toFun := continuous_id
   continuous_invFun := continuous_id
 
@@ -205,17 +207,17 @@ theorem toPartialEquiv_coe : (I.toPartialEquiv : H → E) = I :=
   rfl
 
 @[simp, mfld_simps]
-theorem mk_coe (e : PartialEquiv H E) (a b c d) :
-    ((ModelWithCorners.mk e a b c d : ModelWithCorners 𝕜 E H) : H → E) = (e : H → E) :=
+theorem mk_coe (e : PartialEquiv H E) (a b c d d') :
+    ((ModelWithCorners.mk e a b c d d' : ModelWithCorners 𝕜 E H) : H → E) = (e : H → E) :=
   rfl
 
 @[simp, mfld_simps]
 theorem toPartialEquiv_coe_symm : (I.toPartialEquiv.symm : E → H) = I.symm :=
   rfl
 
 @[simp, mfld_simps]
-theorem mk_symm (e : PartialEquiv H E) (a b c d) :
-    (ModelWithCorners.mk e a b c d : ModelWithCorners 𝕜 E H).symm = e.symm :=
+theorem mk_symm (e : PartialEquiv H E) (a b c d d') :
+    (ModelWithCorners.mk e a b c d d' : ModelWithCorners 𝕜 E H).symm = e.symm :=
   rfl
 
 @[continuity]
@@ -249,6 +251,10 @@ theorem target_eq : I.target = range (I : H → E) := by
 protected theorem uniqueDiffOn : UniqueDiffOn 𝕜 (range I) :=
   I.target_eq ▸ I.uniqueDiffOn'
 
+theorem range_subset_closure_interior : range I ⊆ closure (interior (range I)) := by
+  rw [← I.target_eq]
+  exact I.target_subset_closure_interior
+
 @[deprecated (since := "2024-09-30")]
 protected alias unique_diff := ModelWithCorners.uniqueDiffOn
 
@@ -291,6 +297,9 @@ theorem isClosed_range : IsClosed (range I) :=
 
 @[deprecated (since := "2024-03-17")] alias closed_range := isClosed_range
 
+theorem range_eq_closure_interior : range I = closure (interior (range I)) :=
+  Subset.antisymm I.range_subset_closure_interior I.isClosed_range.closure_interior_subset
+
 theorem map_nhds_eq (x : H) : map I (𝓝 x) = 𝓝[range I] I x :=
   I.isClosedEmbedding.isEmbedding.map_nhds_eq x
 
@@ -353,6 +362,11 @@ protected theorem secondCountableTopology [SecondCountableTopology E] (I : Model
     SecondCountableTopology H :=
   I.isClosedEmbedding.isEmbedding.secondCountableTopology
 
+include I in
+protected theorem t1Space (M : Type*) [TopologicalSpace M] [ChartedSpace H M] : T1Space M := by
+  have : T2Space H := I.isClosedEmbedding.toIsEmbedding.t2Space
+  exact ChartedSpace.t1Space H M
+
 end ModelWithCorners
 
 section
@@ -395,6 +409,9 @@ def ModelWithCorners.prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Ty
     source := { x | x.1 ∈ I.source ∧ x.2 ∈ I'.source }
     source_eq := by simp only [setOf_true, mfld_simps]
     uniqueDiffOn' := I.uniqueDiffOn'.prod I'.uniqueDiffOn'
+    target_subset_closure_interior := by
+      simp only [PartialEquiv.prod_target, target_eq, interior_prod_eq, closure_prod_eq]
+      exact Set.prod_mono I.range_subset_closure_interior I'.range_subset_closure_interior
     continuous_toFun := I.continuous_toFun.prodMap I'.continuous_toFun
     continuous_invFun := I.continuous_invFun.prodMap I'.continuous_invFun }
 
@@ -408,6 +425,9 @@ def ModelWithCorners.pi {𝕜 : Type u} [NontriviallyNormedField 𝕜] {ι : Typ
   toPartialEquiv := PartialEquiv.pi fun i => (I i).toPartialEquiv
   source_eq := by simp only [pi_univ, mfld_simps]
   uniqueDiffOn' := UniqueDiffOn.pi ι E _ _ fun i _ => (I i).uniqueDiffOn'
+  target_subset_closure_interior := by
+    simp only [PartialEquiv.pi_target, target_eq, finite_univ, interior_pi_set, closure_pi_set]
+    exact Set.pi_mono (fun i _ ↦ (I i).range_subset_closure_interior)
   continuous_toFun := continuous_pi fun i => (I i).continuous.comp (continuous_apply i)
   continuous_invFun := continuous_pi fun i => (I i).continuous_symm.comp (continuous_apply i)
 
@@ -441,6 +461,9 @@ theorem modelWithCorners_prod_coe_symm (I : ModelWithCorners 𝕜 E H)
     ((I.prod I').symm : _ × _ → _ × _) = Prod.map I.symm I'.symm :=
   rfl
 
+/-- This lemma should be erased, or at least burn in hell, as it uses bad defeq: the left model
+with corners is for `E times F`, the right one for `ModelProd E F`, and there's a good reason
+we are distinguishing them. -/
 theorem modelWithCornersSelf_prod : 𝓘(𝕜, E × F) = 𝓘(𝕜, E).prod 𝓘(𝕜, F) := by ext1 <;> simp
 
 theorem ModelWithCorners.range_prod : range (I.prod J) = range I ×ˢ range J := by
@@ -861,6 +884,10 @@ theorem nhdsWithin_extend_target_eq {y : M} (hy : y ∈ f.source) :
   (nhdsWithin_mono _ (extend_target_subset_range _)).antisymm <|
     nhdsWithin_le_of_mem (extend_target_mem_nhdsWithin _ hy)
 
+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)
+
 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
@@ -1147,11 +1174,34 @@ 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)
 
+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
+
+theorem extChartAt_target_union_comp_range_mem_nhds_of_mem {y : E} {x : M}
+    (hy : y ∈ (extChartAt I x).target) : (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
+
 /-- 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
 
+
+lemma _root_.Filter.EventuallyEq.mem_interior {α : Type*} [TopologicalSpace α]
+    {x : α} {s t : Set α} (hst : s =ᶠ[𝓝 x] t) (h : x ∈ interior s) :
+    x ∈ interior t := by
+  rw [← nhdsWithin_eq_iff_eventuallyEq] at hst
+  simpa [mem_interior_iff_mem_nhds, ← nhdsWithin_eq_nhds, hst] using h
+
+lemma _root_.Filter.EventuallyEq.mem_interior_iff {α : Type*} [TopologicalSpace α]
+    {x : α} {s t : Set α} (hst : s =ᶠ[𝓝 x] t) :
+    x ∈ interior s ↔ x ∈ interior t :=
+  ⟨fun h ↦ hst.mem_interior h, fun h ↦ hst.symm.mem_interior h⟩
+
 /-- 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
@@ -1170,10 +1220,30 @@ theorem nhdsWithin_extChartAt_target_eq' {x y : M} (hy : y ∈ (extChartAt I x).
     𝓝[(extChartAt I x).target] extChartAt I x y = 𝓝[range I] extChartAt I x y :=
   nhdsWithin_extend_target_eq _ <| by rwa [← extChartAt_source I]
 
+/-- Around a point in the target, `(extChartAt I x).target` and `range I` coincide locally. -/
+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)
+
 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)
 
+/-- Around a point in the target, `(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)
+
+/-- 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)
+
+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)
+
 theorem continuousAt_extChartAt_symm'' {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
     ContinuousAt (extChartAt I x).symm y :=
   continuousAt_extend_symm' _ h
@@ -1190,6 +1260,44 @@ theorem continuousOn_extChartAt_symm (x : M) :
     ContinuousOn (extChartAt I x).symm (extChartAt I x).target :=
   fun _y hy => (continuousAt_extChartAt_symm'' hy).continuousWithinAt
 
+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)ᶜ) ∈ 𝓝 y :=
+    inter_mem ht (extChartAt_target_union_comp_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)ᶜ) ∩ 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
+
+lemma extChartAt_mem_closure_interior {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)) := 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₀).source ∩ interior s).Nonempty := by
+    have : (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 : interior (↑(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)
+
 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
@@ -1275,6 +1383,14 @@ theorem ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range
     ← map_extChartAt_nhdsWithin, nhdsWithin_inter_of_mem']
   exact hc (extChartAt_source_mem_nhds _)
 
+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
+
 /-! We use the name `ext_coord_change` for `(extChartAt I x').symm ≫ extChartAt I x`. -/
 
 theorem ext_coord_change_source (x x' : M) :
@@ -1432,3 +1548,5 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top
 instance : PathConnectedSpace (TangentSpace I x) := inferInstanceAs (PathConnectedSpace E)
 
 end Real
+
+set_option linter.style.longFile 1700