instIsOrderBornology — Mathlib

English

The order dual of a set with a bornology inherits IsOrderBornology.

Русский

Двойственный по порядку набор с борологией наследует IsOrderBornology.

LaTeX

$$$\operatorname{IsOrderBornology}(\alpha^{op})$$$

Lean4

instance instIsOrderBornology : IsOrderBornology αᵒᵈ where
  isBounded_iff_bddBelow_bddAbove
    s := by
    rw [← isBounded_preimage_toDual, ← bddBelow_preimage_toDual, ← bddAbove_preimage_toDual,
      isBounded_iff_bddBelow_bddAbove, and_comm]

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