ofDual_toAdd_zero — Mathlib

English

In a LinearOrderedAddCommMonoidWithTop, the image of zero under the dual multiplicative mapping is top: OrderDual.ofDual (0 : Multiplicative αᵒᵈ).toAdd = ⊤.

Русский

В линейно упорядоченном аддитивном моноиде с вершиной образ нуля под двойственному отображению равен вершине: OrderDual.ofDual (0 : Multiplicative αᵒᵈ).toAdd = ⊤.

LaTeX

$$$OrderDual.ofDual (0 : Multiplicative α^{\\\\circ}) = \\top$$$

Lean4

@[simp]
theorem ofDual_toAdd_zero [LinearOrderedAddCommMonoidWithTop α] : OrderDual.ofDual (0 : Multiplicative αᵒᵈ).toAdd = ⊤ :=
  rfl

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