le_ofDual_iff — Mathlib

English

For x ∈ WithTop α and y ∈ WithTop (OrderDual α), x ≤ ofDual y is equivalent to y ≤ x (under the dualization).

Русский

Для x ∈ WithTop α и y ∈ WithTop (OrderDual α) имеет место: x ≤ ofDual(y) эквивалентно y ≤ x (после двойственности).

LaTeX

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

Lean4

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

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