isMax_ofDual_iff

Mathlib.Order.Max

URI: https://scilib.ai/kg/mathlib#isMax_ofDual_iff

English

The maximum in the dual order corresponds to the minimum in the original order.

Русский

Максимум двойственного порядка соответствует минимуму исходного порядка.

LaTeX

$$$\\\\mathrm{IsMax}(\\\\mathrm{ofDual}(a)) \\\\leftrightarrow \\\\mathrm{IsMin}(a)$$$

Lean4

@[simp]
theorem isMax_ofDual_iff {a : αᵒᵈ} : IsMax (ofDual a) ↔ IsMin a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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