instCardinalInterFilterMap — Mathlib

English

Instance giving CardinalInterFilter for map f l when l has CardinalInterFilter c.

Русский

Инстанс для CardinalInterFilter фильтра map f l при условии, что l имеет CardinalInterFilter c.

LaTeX

$$$CardinalInterFilter(\\mathrm{map}(f, l), c)$$$

Lean4

instance (l : Filter α) [CardinalInterFilter l c] (f : α → β) : CardinalInterFilter (map f l) c :=
  by
  refine ⟨fun S hSc hS => ?_⟩
  simp only [mem_map, sInter_eq_biInter, preimage_iInter₂] at hS ⊢
  exact (cardinal_bInter_mem hSc).2 hS

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