ofAdd_toDual_eq_zero_iff — Mathlib

English

In a LinearOrderedAddCommMonoidWithTop, for x in α, Multiplicative.ofAdd (OrderDual.toDual x) = 0 if and only if x = ⊤.

Русский

В линейном упорядоченном аддитивном моноиде с вершиной, для x ∈ α, Multiplicative.ofAdd (OrderDual.toDual x) = 0 ⇔ x = ⊤.

LaTeX

$$$[LinearOrderedAddCommMonoidWithTop \\\\alpha] (x \\\\in \\\\alpha): \\\\ Multiplicative.ofAdd (OrderDual.toDual x) = 0 \\\\iff x = \\\\top$$$

Lean4

@[simp]
theorem ofAdd_toDual_eq_zero_iff [LinearOrderedAddCommMonoidWithTop α] (x : α) :
    Multiplicative.ofAdd (OrderDual.toDual x) = 0 ↔ x = ⊤ :=
  Iff.rfl

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