comp_left — Mathlib

English

If f has compact multiplicative support and g(1) = 1, then the composition g ∘ f has compact multiplicative support.

Русский

Если у f компактная мультиподдержка и g(1) = 1, то композиция g ∘ f имеет компактную мультиподдержку.

LaTeX

$$$\\text{HasCompactMulSupport}(f) \\land (g(1)=1) \\Rightarrow \\text{HasCompactMulSupport}(g\\circ f).$$$

Lean4

@[to_additive]
theorem comp_left (hf : HasCompactMulSupport f) (hg : g 1 = 1) : HasCompactMulSupport (g ∘ f) :=
  hf.mono <| mulSupport_comp_subset hg f

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