le_generate_iff — Mathlib

English

A filter f is below the generated filter generated by s if and only if s is contained in the sets of f.

Русский

Фильтр f лежит ниже сгенерированного фильтра generate(s) тогда и только тогда, когда s ⊆ f.sets.

LaTeX

$$$ f \le \mathrm{generate}(s) \iff s \subseteq f.{sets}. $$$

Lean4

theorem le_generate_iff {s : Set (Set α)} {f : Filter α} : f ≤ generate s ↔ s ⊆ f.sets :=
  Iff.intro (fun h _ hu => h <| GenerateSets.basic <| hu) fun h _ hu =>
    hu.recOn (fun h' => h h') univ_mem (fun _ hxy hx => mem_of_superset hx hxy) fun _ _ hx hy => inter_mem hx hy

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