instCountableInterFilterComap — Mathlib

English

If l is a CountableInterFilter on β, then comap f l is CountableInterFilter on α.

Русский

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

LaTeX

$$$\\text{instCountableInterFilterComap}(l, f) : CountableInterFilter (Filter.comap f l)$$$

Lean4

instance (l : Filter β) [CountableInterFilter l] (f : α → β) : CountableInterFilter (comap f l) :=
  by
  refine ⟨fun S hSc hS => ?_⟩
  choose! t htl ht using hS
  have : (⋂ s ∈ S, t s) ∈ l := (countable_bInter_mem hSc).2 htl
  refine ⟨_, this, ?_⟩
  simpa [preimage_iInter] using iInter₂_mono ht

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