feat(Analysis/Convex/Intrinsic): add open segment intrinsic interior results

Mathlib/Analysis/Convex/Intrinsic.lean

@@ -5,6 +5,8 @@ Authors: Paul Reichert, Yaël Dillies
 -/
 module
 
+import Mathlib.Analysis.Convex.Topology
+
 public import Mathlib.Analysis.Normed.Affine.AddTorsorBases
 
 /-!
@@ -440,6 +442,31 @@ protected theorem Convex.intrinsicClosure (hs : Convex 𝕜 s) : Convex 𝕜 (in
 
 end Convex
 
+section IntrinsicClosure
+
+variable {E : Type*} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
+  [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
+
+open Homeomorph in
+/-- If `x ∈ intrinsicInterior 𝕜 C` and `y ∈ intrinsicClosure 𝕜 C`, then the open segment
+from `x` to `y` stays in `intrinsicInterior 𝕜 C`. This is the intrinsic-closure form;
+the ambient-closure statement is the finite-dimensional corollary below. -/
+theorem Convex.openSegment_intrinsicInterior_intrinsicClosure_subset_intrinsicInterior {C : Set E}
+    (hC : Convex 𝕜 C) {x y : E} (hx : x ∈ intrinsicInterior 𝕜 C) (hy : y ∈ intrinsicClosure 𝕜 C) :
+    openSegment 𝕜 x y ⊆ intrinsicInterior 𝕜 C := by
+  rcases mem_intrinsicInterior.1 hx with ⟨xA, hxA, rfl⟩
+  rcases mem_intrinsicClosure.1 hy with ⟨yA, hyA, rfl⟩
+  letI : Nonempty (affineSpan 𝕜 C) := ⟨xA⟩
+  let A := (affineSpan 𝕜 C).subtype.comp (AffineEquiv.vaddConst 𝕜 xA).toAffineMap
+  rw [intrinsicInterior, ← (vaddConst xA).image_interior_preimage_comp]
+  intro _ hz
+  simpa [A] using! Convex.openSegment_image_interior_closure_preimage_subset (A := A) hC
+    (by simpa [A] using! ((vaddConst xA).mem_interior_preimage_comp _ 0).2 (by simpa))
+    (by simpa [A] using! ((vaddConst xA).mem_closure_preimage_comp _ (yA -ᵥ xA)).2 (by simpa))
+    (by simpa [A] using hz)
+
+end IntrinsicClosure
+
 private theorem aux {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] (φ : α ≃ₜ β)
     (s : Set β) : (interior s).Nonempty ↔ (interior (φ ⁻¹' s)).Nonempty := by
   rw [← φ.image_symm, ← φ.symm.image_interior, image_nonempty]

Mathlib/Analysis/Convex/Topology.lean

@@ -145,6 +145,22 @@ theorem Convex.openSegment_interior_closure_subset_interior {s : Set E} (hs : Co
   rintro _ ⟨a, b, ha, hb, hab, rfl⟩
   exact hs.combo_interior_closure_mem_interior hx hy ha hb.le hab
 
+omit [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] in
+/-- For a convex set `s`, the open segment between affine images of points in
+`interior (A ⁻¹' s)` and `closure (A ⁻¹' s)` is contained in the affine image of
+`interior (A ⁻¹' s)`. -/
+theorem Convex.openSegment_image_interior_closure_preimage_subset {F : Type*}
+    [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F]
+    [ContinuousConstSMul 𝕜 F] {A : F →ᵃ[𝕜] E} {s} (hs : Convex 𝕜 s)
+    {x y} (hx : x ∈ interior (A ⁻¹' s)) (hy : y ∈ closure (A ⁻¹' s)) :
+    openSegment 𝕜 (A x) (A y) ⊆ A '' interior (A ⁻¹' s) := by
+  rintro _ ⟨a, b, ha, hb, hab, rfl⟩
+  refine ⟨AffineMap.lineMap x y b, ?_, ?_⟩
+  · apply (hs.affine_preimage A).openSegment_interior_closure_subset_interior hx hy
+    refine ⟨a, b, ha, hb, hab, ?_⟩
+    rw [AffineMap.lineMap_apply_module, sub_eq_iff_eq_add.2 hab.symm]
+  · rw [A.apply_lineMap, AffineMap.lineMap_apply_module, sub_eq_iff_eq_add.2 hab.symm]
+
 theorem Convex.openSegment_interior_self_subset_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E}
     (hx : x ∈ interior s) (hy : y ∈ s) : openSegment 𝕜 x y ⊆ interior s :=
   hs.openSegment_interior_closure_subset_interior hx (subset_closure hy)

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -53,6 +53,16 @@ theorem ContinuousNeg.of_continuousConstSMul [ContinuousConstSMul R M] : Continu
 
 end
 
+section Submodule
+
+variable {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M]
+  [ContinuousConstSMul R M]
+
+instance Submodule.continuousConstSMul (S : Submodule R M) : ContinuousConstSMul R S :=
+  IsInducing.subtypeVal.continuousConstSMul id fun {_} {_} => rfl
+
+end Submodule
+
 section
 
 variable {R : Type*} {M : Type*} [Ring R] [TopologicalSpace R] [TopologicalSpace M]

Mathlib/Topology/Homeomorph/Defs.lean

@@ -297,15 +297,30 @@ theorem isClosedEmbedding (h : X ≃ₜ Y) : IsClosedEmbedding h :=
 theorem preimage_closure (h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' closure s = closure (h ⁻¹' s) :=
   h.isOpenMap.preimage_closure_eq_closure_preimage h.continuous _
 
+omit [TopologicalSpace Z] in
+theorem mem_closure_preimage_comp (e : X ≃ₜ Y) (f : Y → Z) {s : Set Z} (x : X) :
+    x ∈ closure ((f ∘ e) ⁻¹' s) ↔ e x ∈ closure (f ⁻¹' s) := by
+  rw [preimage_comp, ← e.preimage_closure, mem_preimage]
+
 theorem image_closure (h : X ≃ₜ Y) (s : Set X) : h '' closure s = closure (h '' s) := by
   rw [← preimage_symm, preimage_closure]
 
 theorem preimage_interior (h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' interior s = interior (h ⁻¹' s) :=
   h.isOpenMap.preimage_interior_eq_interior_preimage h.continuous _
 
+omit [TopologicalSpace Z] in
+theorem mem_interior_preimage_comp (e : X ≃ₜ Y) (f : Y → Z) {s : Set Z} (x : X) :
+    x ∈ interior ((f ∘ e) ⁻¹' s) ↔ e x ∈ interior (f ⁻¹' s) := by
+  rw [preimage_comp, ← e.preimage_interior, mem_preimage]
+
 theorem image_interior (h : X ≃ₜ Y) (s : Set X) : h '' interior s = interior (h '' s) := by
   rw [← preimage_symm, preimage_interior]
 
+omit [TopologicalSpace Z] in
+theorem image_interior_preimage_comp (e : X ≃ₜ Y) (f : Y → Z) (s : Set Z) :
+    (f ∘ e) '' interior ((f ∘ e) ⁻¹' s) = f '' interior (f ⁻¹' s) := by
+  simp only [preimage_comp, image_comp, e.image_interior, image_preimage]
+
 theorem preimage_frontier (h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' frontier s = frontier (h ⁻¹' s) :=
   h.isOpenMap.preimage_frontier_eq_frontier_preimage h.continuous _