mulSupport_comp_eq_of_range_subset

English

If every x in range f satisfies the condition from the previous lemma, then mulSupport(g∘f) = mulSupport(f).

Русский

Если каждый элемент диапазона f удовлетворяет условию, то mulSupport(g∘f) = mulSupport(f).

LaTeX

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

Lean4

@[to_additive]
theorem mulSupport_comp_eq_of_range_subset {g : M → N} {f : ι → M} (hg : ∀ {x}, x ∈ range f → (g x = 1 ↔ x = 1)) :
    mulSupport (g ∘ f) = mulSupport f :=
  Set.ext fun x ↦ not_congr <| by rw [Function.comp, hg (mem_range_self x)]

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