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 |
Demostración en lenguaje natural
Se usarán los siguientes lemas:
\begin{align}
&0 ≤ ab → 0 < b → 0 ≤ a \tag{L1} \\
&d(x,x) = 0 \tag{L2} \\
&d(x,z) ≤ d(x,y) + d(y,z) \tag{L3} \\
&d(x,y) = d(y,x) \tag{L4} \\
&2a = a + a \tag{L5} \\
&0 < 2 \tag{L6} \\
\end{align}
Por L1 es suficiente demostrar las siguientes desigualdades:
\begin{align}
0 &≤ 2d(x,y) \tag{1} \\
0 &< 2 \tag{2}
\end{align}
La (1) se demuestra por las siguiente cadena de desigualdades:
\begin{align}
0 &= d(x,x) &&\text{[por L2]} \\
&≤ d(x,y) + d(y,x) &&\text{[por L3]} \\
&= d(x,y) + d(x,y) &&\text{[por L4]} \\
&= 2 d(x,y) &&\text{[por L5]}
\end{align}
La (2) se tiene por L6.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 |
import Mathlib.Topology.MetricSpace.Basic variable {X : Type _} [MetricSpace X] variable (x y : X) -- 1ª demostración example : 0 ≤ dist x y := by have h1 : 0 ≤ dist x y * 2 := calc 0 = dist x x := (dist_self x).symm _ ≤ dist x y + dist y x := dist_triangle x y x _ = dist x y + dist x y := by rw [dist_comm x y] _ = dist x y * 2 := (mul_two (dist x y)).symm show 0 ≤ dist x y exact nonneg_of_mul_nonneg_left h1 zero_lt_two -- 2ª demostración example : 0 ≤ dist x y := by apply nonneg_of_mul_nonneg_left . -- 0 ≤ dist x y * 2 calc 0 = dist x x := by simp only [dist_self] _ ≤ dist x y + dist y x := by simp only [dist_triangle] _ = dist x y + dist x y := by simp only [dist_comm] _ = dist x y * 2 := by simp only [mul_two] . -- 0 < 2 exact zero_lt_two -- 3ª demostración example : 0 ≤ dist x y := by have : 0 ≤ dist x y + dist y x := by rw [← dist_self x] apply dist_triangle linarith [dist_comm x y] -- 3ª demostración example : 0 ≤ dist x y := -- by apply? dist_nonneg -- Lemas usados -- ============ -- variable (a b : ℝ) -- variable (z : X) -- #check (dist_comm x y : dist x y = dist y x) -- #check (dist_nonneg : 0 ≤ dist x y) -- #check (dist_self x : dist x x = 0) -- #check (dist_triangle x y z : dist x z ≤ dist x y + dist y z) -- #check (mul_two a : a * 2 = a + a) -- #check (nonneg_of_mul_nonneg_left : 0 ≤ a * b → 0 < b → 0 ≤ a) -- #check (zero_lt_two : 0 < 2) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 22.
