instCardinalInterFilterComap — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance (l : Filter β) [CardinalInterFilter l c] (f : α → β) : CardinalInterFilter (comap f l) c :=
  by
  refine ⟨fun S hSc hS => ?_⟩
  choose! t htl ht using hS
  refine ⟨_, (cardinal_bInter_mem hSc).2 htl, ?_⟩
  simpa [preimage_iInter] using iInter₂_mono ht

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