ext — Mathlib

English

An extensionality principle: two filters are equal if they contain exactly the same sets.

Русский

Принцип экстенсиональности: два фильтра равны, если они содержат одинаковые множества.

LaTeX

$$$\forall F,G:\text{Filter}(\alpha),\ (\forall S\subseteq\alpha,\ S\in F \iff S\in G)\Rightarrow F=G$$$

Lean4

@[ext]
protected theorem ext (h : ∀ s, s ∈ f ↔ s ∈ g) : f = g :=
  filter_eq <| Set.ext h

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