le_self_add — Mathlib

English

If x ≠ ⊥ in WithBot α, then for all y, y ≤ y + x holds in WithBot α when α is Add, LE, and CanonicallyOrderedAdd.

Русский

Если x ≠ ⊥ в WithBot α, тогда для любого y выполняется y ≤ y + x в WithBot α при Add, LE и CanonicallyOrderedAdd.

LaTeX

$$$\\forall x \\ne \\bot,\\ \\forall y \\in \\mathrm{WithBot}(\\alpha):\\ y \\le y + x$$$

Lean4

protected theorem le_self_add [Add α] [LE α] [CanonicallyOrderedAdd α] {x : WithBot α} (hx : x ≠ ⊥) (y : WithBot α) :
    y ≤ y + x := by
  induction x
  · simp at hx
  induction y
  · simp
  · rw [← WithBot.coe_add, WithBot.coe_le_coe]
    exact le_self_add

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