cardinalGenerate_isGreatest — Mathlib

English

cardinalGenerate g hc is the greatest cardinalInterFilter c containing g.

Русский

cardinalGenerate g hc является наибольшим CardinalInterFilter c, содержащим g.

LaTeX

$$cardinalGenerate g hc is greatest w.r.t. {f : Filter α | CardinalInterFilter f c ∧ g ⊆ f.sets}.$$

Lean4

/-- `cardinalGenerate g hc` is the greatest `cardinalInterFilter c` containing `g`. -/
theorem cardinalGenerate_isGreatest (hc : 2 < c) :
    IsGreatest {f : Filter α | CardinalInterFilter f c ∧ g ⊆ f.sets} (cardinalGenerate g hc) :=
  by
  refine ⟨⟨cardinalInter_ofCardinalGenerate _ _, fun s => CardinalGenerateSets.basic⟩, ?_⟩
  rintro f ⟨fct, hf⟩
  rwa [le_cardinalGenerate_iff_of_cardinalInterFilter]

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