add_eq_coe — Mathlib

English

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

Русский

Для a,b : WithTop α и c : α, a + b = c эквивалентно существованию a', b' : α таких, что a = some a', b = some b' и a' + b' = c.

LaTeX

$$$\\forall a,b:\\mathrm{WithTop}\\ α,\\; c:\\alpha,\\ a+b=c \\iff \\exists a',b':\\alpha,\\ a=\\mathrm{WithTop}.some a' \\land b=\\mathrm{WithTop}.some b' \\land a'+b'=c$$$

Lean4

theorem add_eq_coe : ∀ {a b : WithTop α} {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

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