isCompact — Mathlib

English

If HasCompactMulSupport f holds, then the set mulTSupport f is compact. In particular, compact multiplicative support implies compactness of the whole multiplicative support.

Русский

Если функция f имеет компактную мультиподдержку, то mulTSupport(f) компактна.

LaTeX

$$$\\text{HasCompactMulSupport}(f) \\;\Rightarrow\\; \\operatorname{IsCompact}(\\operatorname{mulTSupport}(f))$$$

Lean4

@[to_additive]
theorem isCompact (hf : HasCompactMulSupport f) : IsCompact (mulTSupport f) :=
  hf

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