countableGenerate_isGreatest — Mathlib

English

The map g ↦ countableGenerate g is the greatest countable-intersection filter containing g.

Русский

Отображение g ↦ countableGenerate g есть наибольший фильтр с счетным пересечением, содержащий g.

LaTeX

$$$\\text{countableGenerate_isGreatest}(g) : IsGreatest\\{f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets\\} (countableGenerate g)$$$

Lean4

/-- `countableGenerate g` is the greatest `countableInterFilter` containing `g`. -/
theorem countableGenerate_isGreatest :
    IsGreatest {f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets} (countableGenerate g) :=
  by
  refine ⟨⟨inferInstance, fun s => CountableGenerateSets.basic⟩, ?_⟩
  rintro f ⟨fct, hf⟩
  rwa [@le_countableGenerate_iff_of_countableInterFilter _ _ _ fct]

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