addLECancellable_coe — Mathlib

English

For every real x, the addition by x, when viewed inside EReal, is AddLECancellable.

Русский

Для каждого вещественного x добавление x внутри EReal является AddLECancellable.

LaTeX

$$$\\\\forall x \\\\in \\\\mathbb{R},\\\\ AddLECancellable (x \\\\mathrm{:} EReal)$$$

Lean4

theorem addLECancellable_coe (x : ℝ) : AddLECancellable (x : EReal)
  | _, ⊤, _ => le_top
  | ⊥, _, _ => bot_le
  | ⊤, (z : ℝ), h => by simp only [coe_add_top, ← coe_add, top_le_iff, coe_ne_top] at h
  | _, ⊥, h => by simpa using h
  | (y : ℝ), (z : ℝ), h => by simpa only [← coe_add, EReal.coe_le_coe_iff, add_le_add_iff_left] using h

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