mkOfClosure — Mathlib

English

The filter defined by mkOfClosure has its sets exactly equal to S, provided hs holds.

Русский

Фильтр, построенный через mkOfClosure, имеет множества ровно как в S, при условии hs.

LaTeX

$$$\\mathrm{sets}(\\mathrm{mkOfClosure}(S, H)) = S$$$

Lean4

/-- `mkOfClosure s hs` constructs a filter on `α` whose elements set is exactly
`s : Set (Set α)`, provided one gives the assumption `hs : (generate s).sets = s`. -/
protected def mkOfClosure (s : Set (Set α)) (hs : (generate s).sets = s) : Filter α
    where
  sets := s
  univ_sets := hs ▸ univ_mem
  sets_of_superset := hs ▸ mem_of_superset
  inter_sets := hs ▸ inter_mem

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