generate — Mathlib

English

Constructs a filter from an indexed family of sets satisfying IsBasis.

Русский

Строится фильтр из семейства множеств, удовлетворяющего условию IsBasis.

LaTeX

$$$\text{generate } B.sets = B.filter$$$

Lean4

protected theorem generate (B : FilterBasis α) : generate B.sets = B.filter :=
  by
  apply le_antisymm
  · intro U U_in
    rcases B.mem_filter_iff.mp U_in with ⟨V, V_in, h⟩
    exact GenerateSets.superset (GenerateSets.basic V_in) h
  · rw [le_generate_iff]
    apply mem_filter_of_mem

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