filter_eq — Mathlib

English

Two filters on the same space are equal if and only if they have the same membership relation to all subsets.

Русский

Два фильтра на одном пространстве равны тогда и только тогда, когда для любых подмножеств они имеют одинаковое членство.

LaTeX

$$$\forall F,G:\text{Filter}(\alpha),\ (F.sets = G.sets)\Rightarrow F=G$$$

Lean4

theorem filter_eq : ∀ {f g : Filter α}, f.sets = g.sets → f = g
  | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl

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