michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/theories/analysis/real_limit): minor

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-13 15:13:16 -07:00
parent 9fb59a05f5
commit 840f0ea05d
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/theories/analysis/real_limit.lean
View file

@ -21,7 +21,7 @@ These could be avoided in a constructive theory of analysis, but here we will no
follow that route. follow that route.
-/ -/
import .metric_space data.real.complete import .metric_space data.real.complete
open real eq.ops classical open real classical algebra
noncomputable theory noncomputable theory
namespace real namespace real
@ -32,7 +32,7 @@ protected definition to_metric_space [instance] : metric_space ℝ :=
⦃ metric_space, ⦃ metric_space,
dist := λ x y, abs (x - y), dist := λ x y, abs (x - y),
dist_self := λ x, abstract by rewrite [sub_self, abs_zero] end, dist_self := λ x, abstract by rewrite [sub_self, abs_zero] end,
eq_of_dist_eq_zero := @eq_of_abs_sub_eq_zero, eq_of_dist_eq_zero := λ x y, algebra.eq_of_abs_sub_eq_zero,
dist_comm := abs_sub, dist_comm := abs_sub,
dist_triangle := abs_sub_le dist_triangle := abs_sub_le
⦄ ⦄