image_inter_mulSupport_eq — Mathlib

English

For sets and functions, the image interaction with mulSupport satisfies g''s ∩ mulSupport f = g''(s ∩ mulSupport(f ∘ g)).

Русский

Взаимодействие образа и mulSupport: g'' s ∩ mulSupport f = g''(s ∩ mulSupport(f ∘ g)).

LaTeX

$$$ g '' s \cap \operatorname{mulSupport} f = g '' (s \cap \operatorname{mulSupport}(f \circ g)) $$$

Lean4

@[to_additive]
theorem image_inter_mulSupport_eq : g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g)) := by
  rw [mulSupport_comp_eq_preimage f g, image_inter_preimage]

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