lt_toDual_iff — Mathlib

English

For x ∈ WithTop αᵒᵈ and y ∈ WithBot α, x < toDual y is equivalent to y < ofDual x (duality swaps inequalities).

Русский

Для x ∈ WithTop αᵒᵈ и y ∈ WithBot α, неравенство x < toDual(y) эквивалентно y < ofDual(x).

LaTeX

$$$ x < y^{\mathrm{toDual}} \iff y < x^{\mathrm{ofDual}}. $$$$

Lean4

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

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