Two points of a bounded set at equal distances from every point of its relative boundary coincide

Proved

Plasticity.Topology.eq_of_norm_sub_eq_on_intrinsicFrontier

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

Let $C$ be a bounded subset of a real normed space and $x,y\in C$ . If $\|x-b\|=\|y-b\|$ for every point $b$ of the relative boundary of $C$ (its frontier within its affine hull), then $x=y$ . If $x\ne y$ , the ray from $x$ through $y$ leaves $C$ at a relative boundary point $b$ beyond $y$ , and $\|x-b\|>\|y-b\|$ .

Preamble

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

Formal statement

namespace Plasticity.Topology
theorem eq_of_norm_sub_eq_on_intrinsicFrontier {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (C : Set E) (hC : Bornology.IsBounded C) (x y : E) (hx : x ∈ C) (hy : y ∈ C)
    (h : ∀ b ∈ intrinsicFrontier ℝ C, ‖x - b‖ = ‖y - b‖) :
    x = y := by sorry
end Plasticity.Topology

Source

Elementary; used in this repository's proof of the facial covering corollary of claim F17 (expositions/faces/finite_faces_boundary_crossing.md §6) in place of Mankiewicz's extension theorem

View graph