mulTSupport_extend_one — Mathlib

English

If f has compact multiplicative support and g is continuous with g injective, then mulTSupport of g.extend f 1 equals the image of mulTSupport f under g.

Русский

Если mulTSupport f компактна и g непрерывна и инъективна, то mulTSupport(S) расширения равно образ mulTSupport f через g.

LaTeX

$$$\\text{HasCompactMulSupport}(f) \\land \\text{Continuous}(g) \\land \\text{Injective}(g) \\Rightarrow \\operatorname{mulTSupport}(\\text{extend } g f 1) = g\\,''\\operatorname{mulTSupport}(f).$$$

Lean4

@[to_additive]
theorem mulTSupport_extend_one (inj : g.Injective) : mulTSupport (g.extend f 1) = g '' mulTSupport f :=
  (hf.mulTSupport_extend_one_subset cont).antisymm <|
    (image_closure_subset_closure_image cont).trans (closure_mono (mulSupport_extend_one inj).superset)

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