ext_iff_isBounded — Mathlib

English

Two Bornologies on α are equal iff they have the same IsBounded relation for every subset.

Русский

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

LaTeX

$$$t = t' \iff ∀ s, IsBounded_{t}(s) \iff IsBounded_{t'}(s)$$$

Lean4

theorem ext_iff_isBounded {t t' : Bornology α} : t = t' ↔ ∀ s, @IsBounded α t s ↔ @IsBounded α t' s :=
  ext_iff'.trans compl_surjective.forall

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