English
Let X be a topological space of type α with the multiplicative structure given by a space β having a distinguished unit 1. If K ⊆ X is compact and the multiplicative support of f lies inside K, then f has compact multiplicative support. In other words, the set where f deviates from 1 is contained in a compact set, hence its multiplicative support is compact.
Русский
Пусть X — топологическое пространство и имеется умножение со единицей 1. Если K ⊆ X компактен и mulSupport(f) ⊆ K, то mulTSupport(f) компактна. Иными словами, множество точек, где f(x) ≠ 1, лежит в компактном множестве, следовательно, мультиподдержка функции компактна.
LaTeX
$$$\\operatorname{IsCompact}(K) \\wedge \\operatorname{mulSupport}(f) \\subseteq K \\;\Longrightarrow\; \\operatorname{IsCompact}(\\operatorname{mulTSupport}(f))$$$
Lean4
@[to_additive]
theorem of_mulSupport_subset_isCompact [R1Space α] (hK : IsCompact K) (h : mulSupport f ⊆ K) : HasCompactMulSupport f :=
hK.closure_of_subset h
