isOrderBornology_iff_eq_orderBornology

English

An order-bornology on a set is equivalent to the equality of the given bornology with the standard order-bornology.

Русский

Упорядоченная борология на множестве эквивалентна равенству данной борологии с обычной борологией порядка.

LaTeX

$$$\operatorname{IsOrderBornology}(\alpha) \iff \operatorname{Bornology}(\alpha) = \operatorname{orderBornology}$$$

Lean4

theorem isOrderBornology_iff_eq_orderBornology [Lattice α] [Nonempty α] :
    IsOrderBornology α ↔ ‹Bornology α› = orderBornology :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun s ↦ by rw [h, orderBornology_isBounded]⟩⟩
  ext s
  exact isBounded_compl_iff.symm.trans (h.1 _)

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