toDual_le_iff — Mathlib

English

For x ∈ WithBot α and y ∈ WithTop (OrderDual α), the dual order comparison gives x.toDual ≤ y if and only if y ≤ x.toDual (translated back via ofDual).

Русский

Для x ∈ WithBot α и y ∈ WithTop (OrderDual α) неравенство x^{toDual} ≤ y эквивалентно y ≤ x^{toDual} (последнее переводится обратно через ofDual).

LaTeX

$$$ x^{\mathrm{toDual}} \le y \ \Longleftrightarrow\ \mathrm{WithTop.ofDual}(y) \le x^{\mathrm{toDual}}. $$$$

Lean4

theorem toDual_le_iff {x : WithBot α} {y : WithTop αᵒᵈ} : x.toDual ≤ y ↔ WithTop.ofDual y ≤ x := by
  cases x <;> cases y <;> simp [toDual_le]

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