Menu Close

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:

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

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

Escribe un comentario