Real_Addition_is_Well_Defined
Provedproofwikireal-addition
The operation of addition on the set of real numbers R is well-defined.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Real_Addition_is_Well_Defined (x y : ℝ) : x + y = x + y := by sorry
Source