English
For a finite-dimensional real normed vector space E and neighborhood s of x with s ≠ univ, there exists y in frontier s such that infDist x to sᶜ equals dist x y.
Русский
Для конечномерного вещественного нормированного пространства E и окрестности s точки x, s ≠ всего пространства, существует y на границе s с infDist x к sᶜ равным dist(x,y).
LaTeX
$$$\\exists y \\in frontier\\; s,\\; \\text{infDist } x \\; s^c = dist(x,y)$$$
Lean4
/-- If a function has compact support, then either the function is trivial
or the space is finite-dimensional. -/
theorem eq_zero_or_finiteDimensional {X : Type*} [TopologicalSpace X] [Zero X] [T1Space X] {f : E → X}
(hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ FiniteDimensional 𝕜 E :=
(HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup hf h'f).imp_right
fun h ↦
-- TODO: Lean doesn't find the instance without this `have`
have : LocallyCompactSpace E := h;
.of_locallyCompactSpace 𝕜
