theorem
proved
toReal_one
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.RealsFromLogic on GitHub at line 137.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
134instance : LT LogicReal := ⟨fun x y => toReal x < toReal y⟩
135
136@[simp] theorem toReal_zero : toReal (0 : LogicReal) = 0 := toReal_fromReal 0
137@[simp] theorem toReal_one : toReal (1 : LogicReal) = 1 := toReal_fromReal 1
138@[simp] theorem toReal_add (x y : LogicReal) : toReal (x + y) = toReal x + toReal y :=
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