theorem euclideanRelativeInterior_subset_intrinsicInterior (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : euclideanRelativeInterior n C ⊆ intrinsicInterior ℝ C

The book's euclideanRelativeInterior is contained in mathlib's intrinsicInterior in Euclidean space.