ofDual_le_ofDual

Mathlib.Order.Synonym

URI: https://scilib.ai/kg/mathlib#OrderDual.ofDual_le_ofDual

English

For any α with a LE, and a,b ∈ OrderDual α, we have: ofDual a ≤ ofDual b iff b ≤ a.

Русский

Для любых a,b ∈ OrderDual α имеем: ofDual a ≤ ofDual b еквивалентно b ≤ a.

LaTeX

$$$\operatorname{ofDual} a \le \operatorname{ofDual} b \iff b \le a$$$

Lean4

@[simp]
theorem ofDual_le_ofDual [LE α] {a b : αᵒᵈ} : ofDual a ≤ ofDual b ↔ b ≤ a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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