principal — Mathlib

English

The membership between a subset and a filter is equivalent to membership in the filter’s sets family.

Русский

Членство подмножества и фильтра эквивалентно членству в семействах множеств фильтра.

LaTeX

$$$\forall {f:g\, Filter(\alpha)} {s:Set\alpha}, s\in f.sets \iff s\in f$$$

Lean4

/-- The principal filter of `s` is the collection of all supersets of `s`. -/
def principal (s : Set α) : Filter α where
  sets := {t | s ⊆ t}
  univ_sets := subset_univ s
  sets_of_superset hx := Subset.trans hx
  inter_sets := subset_inter

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