Si R es un anillo ordenado y a, b ∈ R, entonces 0 ≤ b – a → a ≤ b

Demostrar que si R es un anillo ordenado y a, b ∈ R, entonces

   0 ≤ b - a → a ≤ b

1	0 ≤ b - a → a ≤ b

Para ello, completar la siguiente teoría de Lean:

import algebra.order.ring
variables {R : Type*} [ordered_ring R]
variables a b : R

example : 0 ≤ b - a → a ≤ b :=
sorry

import algebra.order.ring

variables {R : Type*} [ordered_ring R]

variables a b : R

example : 0 ≤ b - a → a ≤ b :=

sorry

Soluciones con Lean

import algebra.order.ring
variables {R : Type*} [ordered_ring R]
variables a b : R

-- 1ª demostración
-- ===============

example : 0 ≤ b - a → a ≤ b :=
begin
  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
end

-- 2ª demostración
-- ===============

example : 0 ≤ b - a → a ≤ b :=
-- by library_search
sub_nonneg.mp

-- 3ª demostración
-- ===============

example : 0 ≤ b - a → a ≤ b :=
-- by hint
by simp

import algebra.order.ring

variables {R : Type*} [ordered_ring R]

variables a b : R

-- 1ª demostración

-- ===============

example : 0 ≤ b - a → a ≤ b :=

begin

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

end

-- 2ª demostración

-- ===============

example : 0 ≤ b - a → a ≤ b :=

-- by library_search

sub_nonneg.mp

-- 3ª demostración

-- ===============

example : 0 ≤ b - a → a ≤ b :=

-- by hint

by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 23.

Share this:

Escribe un comentarioCancel reply