bddBelow_preimage_ofDual — Mathlib

English

In any preorder, a subset s is bounded below when viewed in the opposite order if and only if it is bounded above in the original order.

Русский

В любой частично упорядоченной множестве множество s, рассмотренное во втором порядке, ограничено снизу тогда и только тогда, когда оно ограничено сверху в исходном порядке.

LaTeX

$$$$ BddBelow_{(\alpha,\le)^{\mathrm{op}}}(s) \iff BddAbove_{(\alpha,\le)}(s) $$$$

Lean4

@[simp]
theorem bddBelow_preimage_ofDual {s : Set α} : BddBelow (ofDual ⁻¹' s) ↔ BddAbove s :=
  Iff.rfl

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