intrinsicInterior_nonempty — Mathlib

English

For a real vector space in finite dimension, intrinsic interior being nonempty is equivalent to the set itself being nonempty, provided the set is convex.

Русский

Для выпуклого множества в конечномерном пространстве внутренность относительно аффинной оболочки непуста тогда и только тогда, когда само множество непусто.

LaTeX

$$$ (\operatorname{intrinsicInterior}_{\mathbb{R}}(s)).\Nonempty \iff s.\Nonempty \quad \text{whenever } \operatorname{Convex}_{\mathbb{R}}(s) $$$

Lean4

theorem intrinsicInterior_nonempty (hs : Convex ℝ s) : (intrinsicInterior ℝ s).Nonempty ↔ s.Nonempty :=
  ⟨by simp_rw [nonempty_iff_ne_empty]; rintro h rfl; exact h intrinsicInterior_empty, Set.Nonempty.intrinsicInterior hs⟩

Похожие утверждения