English
If f and g commute (as embeddings), then the induced Finset maps commute: map f and map g commute.
Русский
Если f и g коммютируют (как вложения), то соответствующие Finset-образы коммутируют.
LaTeX
$$$\mathrm{Commute}(\mathrm{map}\ f, \mathrm{map}\ g)$$$
Lean4
theorem map_filter' (p : α → Prop) [DecidablePred p] (f : α ↪ β) (s : Finset α) [DecidablePred (∃ a, p a ∧ f a = ·)] :
(s.filter p).map f = (s.map f).filter fun b => ∃ a, p a ∧ f a = b := by
simp [Function.comp_def, filter_map, f.injective.eq_iff]