instCountableInterFilterMap — Mathlib

English

If l is CountableInterFilter on α, then map f l has CountableInterFilter on β.

Русский

Если l — CountableInterFilter на α, то map f l имеет CountableInterFilter на β.

LaTeX

$$$\\text{instCountableInterFilterMap}(l)(f) : CountableInterFilter (Filter.map f l)$$$

Lean4

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

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