English
If f has compact multiplicative support and g is a closed embedding, then f ∘ g has compact multiplicative support.
Русский
Если f имеет компактную мультиподдержку и g — замыкательное вложение, то f ∘ g имеет компактную мультиподдержку.
LaTeX
$$$\\text{HasCompactMulSupport}(f) \\Rightarrow \\forall g,\\, \\text{IsClosedEmbedding}(g) \\Rightarrow \\text{HasCompactMulSupport}(f\\circ g).$$$
Lean4
@[to_additive]
theorem comp_isClosedEmbedding (hf : HasCompactMulSupport f) {g : α' → α} (hg : IsClosedEmbedding g) :
HasCompactMulSupport (f ∘ g) :=
by
rw [hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage]
refine IsCompact.of_isClosed_subset (hg.isCompact_preimage hf) isClosed_closure ?_
rw [hg.isEmbedding.closure_eq_preimage_closure_image]
exact preimage_mono (closure_mono <| image_preimage_subset _ _)
