map_filter' — Mathlib

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]

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