mulTSupport_extend_one_subset — Mathlib

English

If f has compact multiplicative support and g is continuous on its domain, then the extension of f by 1 along g is again HasCompactMulSupport.

Русский

Если f имеет компактную мультиподдержку и g непрерывна, то расширение f до значения 1 вдоль g сохраняет компактность мультиподдержки.

LaTeX

$$$\\text{HasCompactMulSupport}(f) \\Rightarrow \\text{HasCompactMulSupport}(g\\extend f\\,1).$$$

Lean4

@[to_additive]
theorem mulTSupport_extend_one_subset : mulTSupport (g.extend f 1) ⊆ g '' mulTSupport f :=
  (hf.image cont).isClosed.closure_subset_iff.mpr <| mulSupport_extend_one_subset.trans (image_mono subset_closure)

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