ofDual_le_ofDual_iff — Mathlib

English

For x,y ∈ WithTop (OrderDual α), the order between their dualified copies corresponds to the reverse order between x and y.

Русский

Для x,y ∈ WithTop (OrderDual α) порядок между их двойственными копиями соответствует обратному порядку между x и y.

LaTeX

$$$ \mathrm{WithTop.ofDual}(x) \le \mathrm{WithTop.ofDual}(y) \iff y \le x. $$$$

Lean4

@[simp]
theorem ofDual_le_ofDual_iff {x y : WithTop αᵒᵈ} : WithTop.ofDual x ≤ WithTop.ofDual y ↔ y ≤ x := by
  cases x <;> cases y <;> simp

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