instLinearOrderedAddCommMonoidWithTopOrderDualAdditive

Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Lean4

instance instLinearOrderedAddCommMonoidWithTopOrderDualAdditive : LinearOrderedAddCommMonoidWithTop (Additive α)ᵒᵈ
    where
  top := .toDual <| .ofMul _
  top_add' := fun a ↦ zero_mul (Additive.toMul (OrderDual.ofDual a))
  le_top := fun a ↦ @zero_le' _ _ (Additive.toMul (OrderDual.ofDual a))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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