En los anillos ordenados, a ≤ b → 0 ≤ b – a
Demostrar con Lean4 que en los anillos ordenados se verifica que
\[ a ≤ b → 0 ≤ b – a \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example : a ≤ b → 0 ≤ b - a := by sorry |
Demostración en lenguaje natural
Se usarán los siguientes lemas:
\begin{align}
&a – a = 0 \tag{L1} \\
&a ≤ b → (∀ c) [a – c ≤ b – c] \tag{L2}
\end{align}
Supongamos que
\[ a ≤ b \tag{1} \]
La demostración se tiene por la siguiente cadena de desigualdades:
\begin{align}
0 &= a – a &&\text{[por L1]} \\
&≤ b – a &&\text{[por (1) y L2]}
\end{align}
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 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) -- 1ª demostración example : a ≤ b → 0 ≤ b - a := by intro h calc 0 = a - a := (sub_self a).symm _ ≤ b - a := sub_le_sub_right h a -- 2ª demostración example : a ≤ b → 0 ≤ b - a := sub_nonneg.mpr -- 3ª demostración example : a ≤ b → 0 ≤ b - a := by simp -- Lemas usados -- ============ -- #check (sub_le_sub_right : a ≤ b → ∀ (c : R), a - c ≤ b - c) -- #check (sub_nonneg : 0 ≤ a - b ↔ b ≤ a) -- #check (sub_self a : a - a = 0) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 22.
