isMax_toDual_iff

Mathlib.Order.Max

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem isMax_toDual_iff : IsMax (toDual a) ↔ IsMin a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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