En los espacios métricos, d(x,y) ≥ 0
Demostrar con Lean4 que en los espacios métricos, \(d(x,y) ≥ 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Topology.MetricSpace.Basic variable {X : Type _} [MetricSpace X] variable (x y : X) example : 0 ≤ d x y := by sorry |