mkOfClosure_sets — Mathlib

English

If the sets of generate S are exactly S, then the filter mkOfClosure S hs equals the generated filter generate S.

Русский

Если множества, образованные порождением S, равны S, тогда mkOfClosure S hs равен generate S.

LaTeX

$$$\\mathrm{mkOfClosure}(S, hs) = \\mathrm{generate}(S)$$$

Lean4

theorem mkOfClosure_sets {s : Set (Set α)} {hs : (generate s).sets = s} : Filter.mkOfClosure s hs = generate s :=
  Filter.ext fun u => show u ∈ (Filter.mkOfClosure s hs).sets ↔ u ∈ (generate s).sets from hs.symm ▸ Iff.rfl

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