ofDual_toAdd_eq_top_iff — Mathlib

English

In a LinearOrderedAddCommMonoidWithTop, for x in Multiplicative(OrderDual α) the equality OrderDual.ofDual x.toAdd = ⊤ is equivalent to x = 0.

Русский

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

LaTeX

$$$Iff \\ (OrderDual.ofDual x.toAdd = \\top) \\ (x = 0)$$$

Lean4

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

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