countableGenerate — Mathlib

English

The countable generate operation produces the greatest countable-intersection filter containing a given collection of sets.

Русский

Операция счетного порождения порождает наибольший фильтр с счетным пересечением, содержащий данную коллекцию множеств.

LaTeX

$$$\\text{countableGenerate} : Set(Set α) \\to Filter α$$$

Lean4

/-- `Filter.countableGenerate g` is the greatest `countableInterFilter` containing `g`. -/
def countableGenerate : Filter α :=
  ofCountableInter (CountableGenerateSets g) (fun _ => CountableGenerateSets.sInter) fun _ _ =>
    CountableGenerateSets.superset
deriving CountableInterFilter

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