of_compactSpace — Mathlib

English

On a compact space, every function has compact multiplicative support.

Русский

На компактном пространстве любая функция имеет компактную мультиподдержку.

LaTeX

$$$\\text{CompactSpace}(\\alpha) \\Rightarrow \\text{HasCompactMulSupport}(f).$$$

Lean4

/-- In a compact space `α`, any function has compact support. -/
@[to_additive]
theorem of_compactSpace (f : α → γ) : HasCompactMulSupport f :=
  IsCompact.of_isClosed_subset isCompact_univ (isClosed_mulTSupport f) (Set.subset_univ (mulTSupport f))

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