ext' — Mathlib

English

If two filters agree on all predicates p (i.e., have the same eventual truth values for p), they are equal.

Русский

Если два фильтра совпадают по всем предикатам p (одинаковые значения в пределах eventual), они равны.

LaTeX

$$$\\forall p, (\\forallᶠ x ∈ f_1, p x) \\iff (\\forallᶠ x ∈ f_2, p x) \\Rightarrow f_1 = f_2$$$

Lean4

protected theorem ext' {f₁ f₂ : Filter α} (h : ∀ p : α → Prop, (∀ᶠ x in f₁, p x) ↔ ∀ᶠ x in f₂, p x) : f₁ = f₂ :=
  Filter.ext h

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