le_toDual_iff — Mathlib

English

For x ∈ WithTop αᵒᵈ and y ∈ WithBot α, x ≤ toDual y is equivalent to y ≤ x.toDual.

Русский

Для x ∈ WithTop αᵒᵈ и y ∈ WithBot α верна эквивалентность: x ≤ toDual(y) ⇔ y ≤ x.toDual.

LaTeX

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

Lean4

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

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