filter_eq_iff — Mathlib

English

Two filters f and g are equal if and only if they have the same membership for every set, i.e., f = g ⇔ f.sets = g.sets.

Русский

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

LaTeX

$$$f = g \iff f.sets = g.sets$$$

Lean4

theorem filter_eq_iff : f = g ↔ f.sets = g.sets :=
  ⟨congr_arg _, filter_eq⟩

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