support_le_prod_of_mem — Mathlib

English

If f ∈ l and l is pairwise disjoint, then the support of f is contained in the support of the product l.prod.

Русский

Если f принадлежит l и l попарно непересекается, то опора f ⊆ опора произведения l.prod.

LaTeX

$$$f\in l\ \wedge\ l.PairswiseDisjoint\Rightarrow \operatorname{supp}(f) \subseteq \operatorname{supp}(l.\mathrm{prod})$$$

Lean4

theorem support_le_prod_of_mem {l : List (Perm α)} (h : f ∈ l) (hl : l.Pairwise Disjoint) :
    f.support ≤ l.prod.support := by
  intro x hx
  rwa [mem_support, ← eq_on_support_mem_disjoint h hl _ hx, ← mem_support]

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