English
HasCompactMulSupport f means the closure of the multiplicative support of f is compact.
Русский
HasCompactMulSupport f означает, что замыкание мультипликативной опоры f компактно.
LaTeX
$$$\operatorname{HasCompactMulSupport}(f) \iff \operatorname{IsCompact}(\operatorname{mulTSupport}(f))$$$
Lean4
/-- A function `f` *has compact multiplicative support* or is *compactly supported* if the closure
of the multiplicative support of `f` is compact. In a T₂ space this is equivalent to `f` being equal
to `1` outside a compact set. -/
@[to_additive /-- A function `f` *has compact support* or is *compactly supported* if the closure of
the support of `f` is compact. In a T₂ space this is equivalent to `f` being equal to `0` outside a
compact set. -/
]
def HasCompactMulSupport (f : α → β) : Prop :=
IsCompact (mulTSupport f)
