English
If f has compact multiplicative support and the multiplicative support of f' lies inside the multiplicative support of f, then f' also has compact multiplicative support.
Русский
Если mulSupport(f') ⊆ mulTSupport(f) и f имеет компактную мультиподдержку, то и f' имеет компактную мультиподдержку.
LaTeX
$$$\\text{HasCompactMulSupport}(f) \\land (\\operatorname{mulSupport}(f') \\subseteq \\operatorname{mulTSupport}(f)) \\Rightarrow \\text{HasCompactMulSupport}(f').$$$
Lean4
@[to_additive]
theorem mono' {f' : α → γ} (hf : HasCompactMulSupport f) (hff' : mulSupport f' ⊆ mulTSupport f) :
HasCompactMulSupport f' :=
IsCompact.of_isClosed_subset hf isClosed_closure <| closure_minimal hff' isClosed_closure
