ofDual_le_ofDual_iff — Mathlib

English

For x,y ∈ WithTop (OrderDual α), WithTop.ofDual x ≤ WithTop.ofDual y iff y ≤ x, expressing compatibility of dual with top-augmented copies.

Русский

Для x,y ∈ WithTop (OrderDual α) верна совместимость двойственности: WithTop.ofDual x ≤ WithTop.ofDual y ⇔ y ≤ x.

LaTeX

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

Lean4

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

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