hasCompactMulSupport_comp_left — Mathlib

English

If for every x, g(x) = 1 is equivalent to x = 1, then HasCompactMulSupport (g ∘ f) is equivalent to HasCompactMulSupport f.

Русский

Если ∀x, g(x)=1 ⇔ x=1, то HasCompactMulSupport(g∘f) эквивалентно HasCompactMulSupport(f).

LaTeX

$$$\\forall x\\, (g(x)=1 \\iff x=1) \\Rightarrow \\text{HasCompactMulSupport}(g\\circ f) \\iff \\text{HasCompactMulSupport}(f).$$$

Lean4

@[to_additive]
theorem _root_.hasCompactMulSupport_comp_left (hg : ∀ {x}, g x = 1 ↔ x = 1) :
    HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f := by
  simp_rw [hasCompactMulSupport_def, mulSupport_comp_eq g (@hg) f]

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