map_filter — Mathlib

English

For an equivalence f: α ≃ β, and p: α → Prop, the image of the filtered set under f equals filtering the mapped set by p ∘ f.symm.

Русский

Для эквивалентности f: α ≃ β и предиката p на α образ отфильтрованного множества через f равен фильтрации образованного множества по p ∘ f.symm.

LaTeX

$$$ (s.filter p).map f.toEmbedding = (s.map f.toEmbedding).filter (p \circ f.symm) $$$

Lean4

theorem map_filter {f : α ≃ β} {p : α → Prop} [DecidablePred p] :
    (s.filter p).map f.toEmbedding = (s.map f.toEmbedding).filter (p ∘ f.symm) := by
  simp only [filter_map, Function.comp_def, Equiv.toEmbedding_apply, Equiv.symm_apply_apply]

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