Convex Analysis (Rockafellar, 1970) -- Chapter 03 -- Section 11 -- Part 3

open scoped Pointwisesection Chap03section Section11

The book's euclideanRelativeInterior (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : Set (EuclideanSpace ℝ (Fin n))euclideanRelativeInterior is contained in mathlib's intrinsicInterior.{u_1, u_2, u_5} (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : Set PintrinsicInterior in Euclidean space.

lemma euclideanRelativeInterior_subset_intrinsicInterior (n : Nat)
    (C : Set (EuclideanSpace Real (Fin n))) :
    euclideanRelativeInterior n C ⊆ intrinsicInterior Real C := by
  classical
  intro x hx
  rcases hx with ⟨hx_aff, ε, hε, hxsub⟩
  let A : AffineSubspace Real (EuclideanSpace Real (Fin n)) := affineSpan Real C
  let sA : Set A := ((↑) : A → EuclideanSpace Real (Fin n)) ⁻¹' C
  refine (mem_intrinsicInterior).2 ?_
  refine ⟨(⟨x, hx_aff⟩ : A), ?_, rfl⟩
  have hball : Metric.ball (⟨x, hx_aff⟩ : A) ε ⊆ sA := by
    intro y hy
    have hyBall : dist (y : EuclideanSpace Real (Fin n)) x < ε := by
      simpa using hy
    have hyClosed : (y : EuclideanSpace Real (Fin n)) ∈ Metric.closedBall x ε :=
      (Metric.mem_closedBall).2 (le_of_lt hyBall)
    have hclosed :
        (fun z : EuclideanSpace Real (Fin n) => x + z) '' (ε • euclideanUnitBall n) =
          Metric.closedBall x ε := by
      simpa using (translate_smul_unitBall_eq_closedBall n x ε hε)
    have hyLeft :
        (y : EuclideanSpace Real (Fin n)) ∈
          (fun z : EuclideanSpace Real (Fin n) => x + z) '' (ε • euclideanUnitBall n) := by
      simpa [hclosed] using hyClosed
    have hyC : (y : EuclideanSpace Real (Fin n)) ∈ C := hxsub ⟨hyLeft, y.property⟩
    simpa [sA] using hyC
  have hsA_nhds : sA ∈ nhds (⟨x, hx_aff⟩ : A) :=
    Metric.mem_nhds_iff.2 ⟨ε, hε, hball⟩
  exact (mem_interior_iff_mem_nhds).2 hsA_nhds

end Section11end Chap03