card_support_prod_list_of_pairwise_disjoint

English

If l is a pairwise disjoint list of permutations, then the support of l.prod has size equal to the sum of the sizes of the supports of the elements of l.

Русский

Если l — попарно непересекающийся список перестановок, то опора l.prod имеет размер, равный сумме размеров опор элементов l.

LaTeX

$$$\#(l.\mathrm{prod}).\operatorname{support} = (l.\mathrm{map} (\mathrm{card} \circ \mathrm{support})).\sum$$$

Lean4

theorem card_support_prod_list_of_pairwise_disjoint {l : List (Perm α)} (h : l.Pairwise Disjoint) :
    #l.prod.support = (l.map (card ∘ support)).sum := by
  induction l with
  | nil => exact card_support_eq_zero.mpr rfl
  | cons a t ih =>
    obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h
    rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]
    exact (disjoint_prod_right _ ha).card_support_mul

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