ext_iff' — Mathlib

English

Two Bornologies on α are equal if and only if every subset of α has the same cobounded membership under both bornologies.

Русский

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

LaTeX

$$$t = t' \iff \forall s, s \in cobounded\, t \iff s \in cobounded\, t'$$$

Lean4

theorem ext_iff' {t t' : Bornology α} : t = t' ↔ ∀ s, s ∈ @cobounded α t ↔ s ∈ @cobounded α t' :=
  Bornology.ext_iff.trans Filter.ext_iff

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