le_cardinalGenerate_iff_of_cardinalInterFilter

English

For any f with CardinalInterFilter f c, f ≤ cardinalGenerate g hc iff g ⊆ f.sets.

Русский

Для любого f с CardinalInterFilter f c верно: f ≤ cardinalGenerate g hc тогда и только тогда, когда g ⊆ f.sets.

LaTeX

$$$f \le cardinalGenerate(g, hc) \iff g \subseteq f.sets$$$

Lean4

theorem le_cardinalGenerate_iff_of_cardinalInterFilter {f : Filter α} [CardinalInterFilter f c] (hc : 2 < c) :
    f ≤ cardinalGenerate g hc ↔ g ⊆ f.sets := by
  constructor <;> intro h
  · exact subset_trans (fun s => CardinalGenerateSets.basic) h
  intro s hs
  induction hs with
  | basic hs => exact h hs
  | univ => exact univ_mem
  | superset _ st ih => exact mem_of_superset ih st
  | sInter Sct _ ih => exact (cardinal_sInter_mem Sct).mpr ih

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