smallSets_comap_eq_comap_image — Mathlib

English

The smallSets of a comap filter equals the comap of the smallSets obtained by mapping f.

Русский

Малые множества фильтра-комапа равны комапу малого множества, полученного приложением f.

LaTeX

$$$ (\\\\mathrm{comap} f \\\\text{l}).smallSets = \\\\mathrm{comap} (\\\\mathrm{image} f) \\\\text{l.smallSets} $$$

Lean4

theorem smallSets_comap_eq_comap_image (l : Filter β) (f : α → β) :
    (comap f l).smallSets = comap (image f) l.smallSets :=
  by
  refine (gc_map_comap _).u_comm_of_l_comm (gc_map_comap _) bind_smallSets_gc bind_smallSets_gc ?_
  simp [Function.comp_def, map_bind, bind_map]

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