addLECancellable_of_lt_bot — Mathlib

English

If α is Preorder and AddLeftReflectLE, and x < ⊥ in WithBot α, then AddLECancellable x.

Русский

Если α — предпорядок и AddLeftReflectLE, и x < ⊥ в WithBot α, тогда AddLECancellable x.

LaTeX

$$$$\\forall x \\in \\mathrm{WithBot}(\\alpha),\\ x < \\bot \\Rightarrow \\text{AddLECancellable } x.$$$$

Lean4

theorem addLECancellable_of_lt_bot [Preorder α] [AddLeftReflectLE α] (hx : x < ⊥) : AddLECancellable x :=
  addLECancellable_of_ne_bot hx.ne

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