addLECancellable_iff_ne_top — Mathlib

English

If there exist a nonempty α with a suitable order and left-reflecting LE, then AddLECancellable x is equivalent to x ≠ ⊤.

Русский

При наличии непустого α с подходящим порядком и левым отражающим LE, AddLECancellable x эквивалентно x ≠ ⊤.

LaTeX

$$$\\\\forall {\\\\alpha} [Nonempty \\\\alpha] [Preorder \\\\alpha] [AddLeftReflectLE \\\\alpha], AddLECancellable x \\\\Leftrightarrow x \\\\neq \\\\top$$$

Lean4

theorem addLECancellable_iff_ne_top [Nonempty α] [Preorder α] [AddLeftReflectLE α] : AddLECancellable x ↔ x ≠ ⊤
    where
  mp := by rintro h rfl; exact (coe_lt_top <| Classical.arbitrary _).not_ge <| h <| by simp
  mpr := addLECancellable_of_ne_top

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