toDual_le_toDual_iff

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.toDual_le_toDual_iff

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

@[simp]
theorem toDual_le_toDual_iff {x y : WithTop α} : x.toDual ≤ y.toDual ↔ y ≤ x := by
  cases x <;> cases y <;> simp [le_toDual]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru