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