Theorems · Theorem · general topology

Filter.mem_countableGenerate_iff

∀ {α : Type u_2} {g : Set (Set α)} {s : Set α}, s ∈ Filter.countableGenerate g ↔ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

A set is in the countableInterFilter generated by g if and only if it contains a countable intersection of elements of g.

Defined in

Mathlib.Order.Filter.CountableInter

Cited by

1 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound