generate — Mathlib

English

If U ∈ s then U ∈ generate s; the generating process contains all generating members.

Русский

Если U ∈ s, тогда U ∈ generate s; порождение содержит все порождающие множества.

LaTeX

$$$ U \in s \Rightarrow U \in \mathrm{generate}(s). $$$

Lean4

/-- `generate g` is the largest filter containing the sets `g`. -/
def generate (g : Set (Set α)) : Filter α
    where
  sets := {s | GenerateSets g s}
  univ_sets := GenerateSets.univ
  sets_of_superset := GenerateSets.superset
  inter_sets := GenerateSets.inter

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