add_eq_coe — Mathlib

English

For all a,b : WithBot α and c : α, a + b = c iff there exist a', b' : α with a = some a' and b = some b' and a' + b' = c.

Русский

Для всех a,b : WithBot α и c : α, a + b = c тогда и только тогда, когда существуют a', b' : α такие, что a = some a', b = some b' и a' + b' = c.

LaTeX

$$$ \\forall a,b:\\mathrm{WithBot}\\,\\alpha \\;\\forall c:\\alpha,\\ a + b = c \\iff \\exists a',b' : \\alpha, \\ (↑a' = a) \\land (↑b' = b) \\land a' + b' = c $$$

Lean4

theorem add_eq_coe : ∀ {a b : WithBot α} {c : α}, a + b = c ↔ ∃ a' b' : α, ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
  | ⊥, b, c => by simp
  | some a, ⊥, c => by simp
  | some a, some b, c => by norm_cast; simp

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