eq_one_or_finiteDimensional — Mathlib

English

If a function has compact support, then either it is identically zero or the space is finite-dimensional.

Русский

Если функция имеет компактную опору, то либо она нулевая, либо пространство конечномомерно.

LaTeX

$$$\\text{HasCompactSupport } f \\Rightarrow (f=0 \\;\u2227\\; \\text{FiniteDimensional } 𝕜 E)$$$

Lean4

/-- If a function has compact multiplicative support, then either the function is trivial
or the space is finite-dimensional. -/
@[to_additive existing]
theorem eq_one_or_finiteDimensional {X : Type*} [TopologicalSpace X] [One X] [T1Space X] {f : E → X}
    (hf : HasCompactMulSupport f) (h'f : Continuous f) : f = 1 ∨ FiniteDimensional 𝕜 E :=
  have : T1Space (Additive X) := ‹_›
  HasCompactSupport.eq_zero_or_finiteDimensional (X := Additive X) 𝕜 hf h'f

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