addLECancellable_coe — Mathlib

English

For any a ∈ α, the element a treated as WithBot α is AddLECancellable, given LE α and AddLeftReflectLE α.

Русский

Для любого a ∈ α элемент a внутри WithBot α является AddLECancellable, при LE α и AddLeftReflectLE α.

LaTeX

$$$$\\forall a \\in \\alpha,\\ \\text{AddLECancellable}(a: \\mathrm{WithBot}(\\alpha)).$$$$

Lean4

theorem addLECancellable_coe [LE α] [AddLeftReflectLE α] (a : α) : AddLECancellable (a : WithBot α) :=
  addLECancellable_of_ne_bot coe_ne_bot

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