coext — Mathlib

English

If for every set s, s^c ∈ f ↔ s^c ∈ g, then f = g.

Русский

Если для каждого множества s верно s^c ∈ f ↔ s^c ∈ g, то f = g.

LaTeX

$$$\forall s, s^{c} \in f \iff s^{c} \in g \Rightarrow f = g$$$

Lean4

/-- An extensionality lemma that is useful for filters with good lemmas about `sᶜ ∈ f` (e.g.,
`Filter.comap`, `Filter.coprod`, `Filter.Coprod`, `Filter.cofinite`). -/
protected theorem coext (h : ∀ s, sᶜ ∈ f ↔ sᶜ ∈ g) : f = g :=
  Filter.ext <| compl_surjective.forall.2 h

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