le_add_self — Mathlib

English

If x ≠ ⊥ in WithBot α, then for all y, y ≤ x + y holds in WithBot α, given AddCommMagma α, LE α, and CanonicallyOrderedAdd α.

Русский

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

LaTeX

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

Lean4

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

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