bddBelow_preimage_toDual — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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