theorem
proved
toReal_sub
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.RealsFromLogic on GitHub at line 142.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
139 toReal_fromReal _
140@[simp] theorem toReal_neg (x : LogicReal) : toReal (-x) = -toReal x :=
141 toReal_fromReal _
142@[simp] theorem toReal_sub (x y : LogicReal) : toReal (x - y) = toReal x - toReal y :=
143 toReal_fromReal _
144@[simp] theorem toReal_mul (x y : LogicReal) : toReal (x * y) = toReal x * toReal y :=
145 toReal_fromReal _
146@[simp] theorem toReal_inv (x : LogicReal) : toReal x⁻¹ = (toReal x)⁻¹ :=
147 toReal_fromReal _
148@[simp] theorem toReal_div (x y : LogicReal) : toReal (x / y) = toReal x / toReal y :=
149 toReal_fromReal _
150
151theorem le_iff_toReal_le {x y : LogicReal} : x ≤ y ↔ toReal x ≤ toReal y := Iff.rfl
152theorem lt_iff_toReal_lt {x y : LogicReal} : x < y ↔ toReal x < toReal y := Iff.rfl
153
154theorem add_assoc' (x y z : LogicReal) : (x + y) + z = x + (y + z) := by
155 rw [eq_iff_toReal_eq]
156 simp
157 ring
158
159theorem add_comm' (x y : LogicReal) : x + y = y + x := by
160 rw [eq_iff_toReal_eq]
161 simp
162 ring
163
164theorem zero_add' (x : LogicReal) : (0 : LogicReal) + x = x := by
165 rw [eq_iff_toReal_eq]
166 simp
167
168theorem add_zero' (x : LogicReal) : x + (0 : LogicReal) = x := by
169 rw [eq_iff_toReal_eq]
170 simp
171
172theorem add_left_neg' (x : LogicReal) : -x + x = 0 := by