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 |
Read More «Si X es un espacio métrico y x, y ∈ X, entonces dist(x,y) ≥ 0»