A point of a set lies in its relative interior iff a small ball of its direction space around the point stays in the set

Proved

Plasticity.Topology.mem_intrinsicInterior_iff_ball

by scanstone · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

Let $C$ be a subset of a real normed space and $x$ a point of the space. Then $x$ lies in the relative interior of $C$ (its interior within the affine hull) if and only if there is $\varepsilon>0$ with $x+w\in C$ for every $w$ in the linear span of $C-C$ with $\|w\|<\varepsilon$ .

Preamble

import Mathlib.Analysis.Normed.Module.Basic
import Mathlib.Analysis.Convex.Intrinsic

Formal statement

namespace Plasticity.Topology
theorem mem_intrinsicInterior_iff_ball {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (C : Set E) (x : E) :
    x ∈ intrinsicInterior ℝ C ↔ ∃ ε > 0, ∀ w ∈ vectorSpan ℝ C, ‖w‖ < ε → x + w ∈ C := by sorry
end Plasticity.Topology

Source

Elementary; Mathlib's intrinsicInterior

View graph