isTotal_le

Mathlib.Order.RelClasses

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

English

If α has a total order, then the dual order αᵒᵈ also has a total ≤-order.

Русский

Если у типа α есть полный порядок, то двойственный порядок αᵒᵈ также имеет полный порядок по ≤.

LaTeX

$$$\mathrm{IsTotal}(\alpha^{\mathrm{op}}, \le)$$$

Lean4

instance isTotal_le [LE α] [h : IsTotal α (· ≤ ·)] : IsTotal αᵒᵈ (· ≤ ·) :=
  @IsTotal.swap α _ h

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

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

Разделы

Аффилиация

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