English
Let s be a finite set of indices and f a function to a monoid β. If the elements f(a) commute pairwise for a in s, then the image set {f(a) : a ∈ s} consists of pairwise-commuting elements in β.
Русский
Пусть s — конечное множество индексов и f — функция в моноид β. Если элементы f(a) коммутируют попарно для всех a ∈ s, тогда образ {f(a) : a ∈ s} состоит из попарно коммутирующих элементов в β.
LaTeX
$$$ (s : \mathrm{Finset} \; \alpha) \; (f : \alpha \to \beta) \; (comm : (s : \mathrm{Set} \alpha).{\rm Pairwise} (\mathrm{Commute} \; {\rm on} \; f)) \Rightarrow \mathrm{Set}.Pairwise \{x \mid x \in \mathrm{Multiset.map} f s.\mathrm{val}\} \; \mathrm{Commute}$$$
Lean4
/-- Proof used in definition of `Finset.noncommProd` -/
@[to_additive]
theorem noncommProd_lemma (s : Finset α) (f : α → β) (comm : (s : Set α).Pairwise (Commute on f)) :
Set.Pairwise {x | x ∈ Multiset.map f s.val} Commute :=
by
simp_rw [Multiset.mem_map]
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ _
exact comm.of_refl ha hb
