addLECancellable_iff_ne_bot — Mathlib

English

For nonempty α with Preorder α and AddLeftReflectLE α, AddLECancellable x holds iff x ≠ ⊥.

Русский

Для непустого α с предорядком и AddLeftReflectLE α, AddLECancellable x тогда и только тогда, когда x ≠ ⊥.

LaTeX

$$$$\\forall x \\in \\mathrm{WithBot}(\\alpha),\\ \\mathrm{AddLECancellable}(x) \\iff x \\neq \\bot.$$$$

Lean4

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

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