mulSupport_subset_comp — Mathlib

English

If for all x, g(x)=1 implies x=1, then the support of f is contained in the support of g∘f.

Русский

Если для всех x, g(x)=1 ⇒ x=1, то mulSupport(f) ⊆ mulSupport(g∘f).

LaTeX

$$$ \bigl(\forall x, \ g x = 1 \Rightarrow x = 1\bigr) \Rightarrow \operatorname{mulSupport}(f) \subseteq \operatorname{mulSupport}(g \circ f) $$$

Lean4

@[to_additive]
theorem mulSupport_subset_comp {g : M → N} (hg : ∀ {x}, g x = 1 → x = 1) (f : ι → M) :
    mulSupport f ⊆ mulSupport (g ∘ f) := fun _ ↦ mt hg

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