bddAbove_preimage_ofDual — Mathlib

English

A subset s is bounded above in the dual order if and only if it is bounded below in the original order.

Русский

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

LaTeX

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

Lean4

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

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