Si X es un espacio métrico y x, y ∈ X, entonces dist(x,y) ≥ 0
Demostrar que si X es un espacio métrico y x, y ∈ X, entonces
|
1 |
0 ≤ dist x y |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import topology.metric_space.basic variables {X : Type*} [metric_space X] variables x y : X example : 0 ≤ dist x y := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 |
import topology.metric_space.basic variables {X : Type*} [metric_space X] variables x y : X -- 1ª demostración example : 0 ≤ dist x y := have h1 : 2 * dist x y ≥ 0, by calc 2 * dist x y = dist x y + dist x y : two_mul (dist x y) ... = dist x y + dist y x : by rw [dist_comm x y] ... ≥ dist x x : dist_triangle x y x ... = 0 : dist_self x, show 0 ≤ dist x y, by exact nonneg_of_mul_nonneg_left h1 zero_lt_two -- 2ª demostración example : 0 ≤ dist x y := -- by library_search dist_nonneg |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 24.
