instMembership — Mathlib

English

Membership between a subset of α and a filter F is defined by membership of the subset in the family of sets of F.

Русский

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

LaTeX

$$$\forall F:\text{Filter}(\alpha),\ \forall s:\mathcal P(\alpha),\ s\in F \iff s\in F.sets$$$

Lean4

/-- If `F` is a filter on `α`, and `U` a subset of `α` then we can write `U ∈ F` as on paper. -/
instance instMembership : Membership (Set α) (Filter α) :=
  ⟨fun F U => U ∈ F.sets⟩

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