bddAbove_preimage_toDual — Mathlib

English

For a subset s ⊆ αᵒᵈ, being bounded above in the dual order is equivalent to being bounded below in the original order.

Русский

Для множества s ⊆ αᵒᵈ, ограниченность сверху во втором порядке эквивалентна ограниченности снизу в исходном порядке.

LaTeX

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

Lean4

@[simp]
theorem bddAbove_preimage_toDual {s : Set αᵒᵈ} : BddAbove (toDual ⁻¹' s) ↔ BddBelow s :=
  Iff.rfl

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