support_mul_le — Mathlib

English

The support of the product f g is contained in the union of supports of f and g.

Русский

Поддержка произведения f g содержится в объединении поддержек f и g.

LaTeX

$$$$ (f g).\operatorname{support} \subseteq f.\operatorname{support} \cup g.\operatorname{support}. $$$$

Lean4

theorem support_mul_le (f g : Perm α) : (f * g).support ≤ f.support ⊔ g.support := fun x =>
  by
  simp only [sup_eq_union]
  rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
  rintro ⟨hf, hg⟩
  rw [hg, hf]

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