extend_one — Mathlib

English

For a HasCompactMulSupport f with a continuous g, the multiplicative support of the extended function is contained in the image of mulTSupport f under g.

Русский

Мультиподдержка расширенной функции лежит внутри образа mulTSupport f под g.

LaTeX

$$$\\operatorname{mulTSupport}(\\text{extend } g f 1) \\subseteq g''(\\operatorname{mulTSupport}(f)).$$$

Lean4

@[to_additive]
theorem extend_one : HasCompactMulSupport (g.extend f 1) :=
  HasCompactMulSupport.of_mulSupport_subset_isCompact (hf.image cont)
    (subset_closure.trans <| hf.mulTSupport_extend_one_subset cont)

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