English
The collection of filters on a type α is equipped with a partial order given by reverse inclusion of their members: for filters f and g, f ≤ g if and only if every set that belongs to g also belongs to f.
Русский
Множество фильтров на α снабжается отношением частичного порядка, заданным обратным включением их множеств: для фильтров f и g верно f ≤ g тогда и только тогда, когда любое множество, принадлежащее g, принадлежит и f.
LaTeX
$$$f \\le g \\iff \\forall U : Set \\alpha, U \\in g \\to U \\in f$$$
Lean4
instance : PartialOrder (Filter α) where
le f g := ∀ ⦃U : Set α⦄, U ∈ g → U ∈ f
le_antisymm a b h₁ h₂ := filter_eq <| Subset.antisymm h₂ h₁
le_refl a := Subset.rfl
le_trans a b c h₁ h₂ := Subset.trans h₂ h₁
