English
In a finite-dimensional real normed space, the intrinsic interior of a nonempty convex set is nonempty.
Русский
В конечномерном вещественном нормированном пространстве внутренность относительно аффинной оболочки выпуклого множества непуста, если множество непустое.
LaTeX
$$$ \operatorname{Convex}_{\mathbb{R}}(s) \Rightarrow s \neq \emptyset \Rightarrow (\operatorname{intrinsicInterior}_{\mathbb{R}}(s)) \neq \emptyset $$$
Lean4
/-- The intrinsic interior of a nonempty convex set is nonempty. -/
protected theorem intrinsicInterior (hscv : Convex ℝ s) (hsne : s.Nonempty) : (intrinsicInterior ℝ s).Nonempty :=
by
haveI := hsne.coe_sort
obtain ⟨p, hp⟩ := hsne
let p' : _root_.affineSpan ℝ s := ⟨p, subset_affineSpan _ _ hp⟩
rw [intrinsicInterior, image_nonempty, aux (AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph,
Convex.interior_nonempty_iff_affineSpan_eq_top, AffineIsometryEquiv.coe_toHomeomorph, ←
AffineIsometryEquiv.coe_toAffineEquiv, ← comap_span, affineSpan_coe_preimage_eq_top, comap_top]
exact
hscv.affine_preimage
((_root_.affineSpan ℝ s).subtype.comp (AffineIsometryEquiv.constVSub ℝ p').symm.toAffineEquiv.toAffineMap)
