countableInter_ofCountableInter — Mathlib

English

If l is a filter with CountableInterFilter and f: α → β, then comap f l is a CountableInterFilter.

Русский

Если l — фильтр с CountableInterFilter и f: α → β, то образованный фильтр comap f l также имеет счетное пересечение.

LaTeX

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

Lean4

instance countableInter_ofCountableInter (l : Set (Set α)) (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l)
    (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : CountableInterFilter (Filter.ofCountableInter l hl h_mono) :=
  ⟨hl⟩

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