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