le_countableGenerate_iff_of_countableInterFilter

English

For f with CountableInterFilter, f ≤ countableGenerate g iff g ⊆ f.sets.

Русский

Для f с CountableInterFilter верно: f ≤ countableGenerate g тогда как g ⊆ f.sets.

LaTeX

$$$f ≤ countableGenerate g \\iff g ⊆ f.sets$$$

Lean4

theorem le_countableGenerate_iff_of_countableInterFilter {f : Filter α} [CountableInterFilter f] :
    f ≤ countableGenerate g ↔ g ⊆ f.sets := by
  constructor <;> intro h
  · exact subset_trans (fun s => CountableGenerateSets.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 (countable_sInter_mem Sct).mpr ih

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