toDual_lt_iff — Mathlib

English

For x,y ∈ WithBot α, the duality respects the order relation when comparing their duals: x.toDual ≤ y.toDual ⇔ y ≤ x.

Русский

Дуальность сохраняет отношение порядка при сравнении их дуалей: x^{toDual} ≤ y^{toDual} ⇔ y ≤ x.

LaTeX

$$$ x^{\mathrm{toDual}} \le y^{\mathrm{toDual}} \iff y \le x. $$$$

Lean4

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

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