Anillos ordenados – Calculemus

En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc

PorJosé A. Alonso 29 septiembre 202310 septiembre 2023

Demostrar con Lean4 que, en los anillos ordenados,
$\{a ≤ b, 0 ≤ c\} ⊢ ac ≤ bc$

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
  (h1 : a ≤ b)
  (h2 : 0 ≤ c)
  : a * c ≤ b * c :=
by sorry

import Mathlib.Algebra.Order.Ring.Defs

variable {R : Type _} [StrictOrderedRing R]

variable (a b c : R)

example

(h1 : a ≤ b)

(h2 : 0 ≤ c)

: a * c ≤ b * c :=

by sorry

En los anillos ordenados, 0 ≤ b – a → a ≤ b

PorJosé A. Alonso 28 septiembre 202310 septiembre 2023

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

import Mathlib.Algebra.Order.Ring.Defs

variable {R : Type _} [StrictOrderedRing R]

variable (a b c : R)

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

by sorry

En los anillos ordenados, a ≤ b → 0 ≤ b – a

PorJosé A. Alonso 27 septiembre 20239 septiembre 2023

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:

import Mathlib.Algebra.Order.Ring.Defs
variable {R : Type _} [StrictOrderedRing R]
variable (a b c : R)

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

import Mathlib.Algebra.Order.Ring.Defs

variable {R : Type _} [StrictOrderedRing R]

variable (a b c : R)

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

by sorry

Si R es un anillo ordenado y a, b, c ∈ R tales que a ≤ b y 0 ≤ c, entonces ac ≤ bc

PorJosé A. Alonso 28 octubre 202225 octubre 2022

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

   a ≤ b 
   0 ≤ c

1 2	a ≤ b 0 ≤ c

entonces

   a * c ≤ b * c

1	a * c ≤ b * c

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

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

example
  (h1 : a ≤ b)
  (h2 : 0 ≤ c)
  : a * c ≤ b * c :=
sorry

import algebra.order.ring

variables {R : Type*} [ordered_ring R]

variables a b c: R

example

(h1 : a ≤ b)

(h2 : 0 ≤ c)

: a * c ≤ b * c :=

sorry

Soluciones con Lean

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

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

example
  (h1 : a ≤ b)
  (h2 : 0 ≤ c)
  : a * c ≤ b * c :=
begin
  have h3 : 0 ≤ b - a :=
    sub_nonneg.mpr h1,
  have h4 : 0 ≤ (b - a) * c :=
    mul_nonneg h3 h2,
  have h5 : (b - a) * c = b * c - a * c :=
    sub_mul b a c,
  have h6 : 0 ≤ b * c - a * c :=
    eq.trans_ge h5 h4,
  show a * c ≤ b * c,
    by exact sub_nonneg.mp h6,
end

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

open_locale classical

example
  (h1 : a ≤ b)
  (h2 : 0 ≤ c)
  : a * c ≤ b * c :=
begin
  by_cases h3 : b ≤ a,
  { have h3a : a = b :=
      le_antisymm h1 h3,
    show a * c ≤ b * c,
      by rw h3a },
  { by_cases h4 : c = 0,
    { calc a * c = a * 0 : by rw h4
             ... = 0     : by rw mul_zero
             ... ≤ 0     : le_refl 0
             ... = b * 0 : by rw mul_zero
             ... = b * c : by {congr ; rw h4}},
    { apply le_of_lt,
      apply mul_lt_mul_of_pos_right,
      { show a < b,
          by exact lt_of_le_not_le h1 h3 },
      { show 0 < c,
          by exact lt_of_le_of_ne h2 (ne.symm h4) }}},
end

-- 3ª demostración
example
  (h1 : a ≤ b)
  (h2 : 0 ≤ c)
  : a * c ≤ b * c :=
-- by library_search
mul_le_mul_of_nonneg_right h1 h2

import algebra.order.ring

variables {R : Type*} [ordered_ring R]

variables a b c: R

-- 1ª demostración

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

example

(h1 : a ≤ b)

(h2 : 0 ≤ c)

: a * c ≤ b * c :=

begin

have h3 : 0 ≤ b - a :=

sub_nonneg.mpr h1,

have h4 : 0 ≤ (b - a) * c :=

mul_nonneg h3 h2,

have h5 : (b - a) * c = b * c - a * c :=

sub_mul b a c,

have h6 : 0 ≤ b * c - a * c :=

eq.trans_ge h5 h4,

show a * c ≤ b * c,

by exact sub_nonneg.mp h6,

end

-- 2ª demostración

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

open_locale classical

example

(h1 : a ≤ b)

(h2 : 0 ≤ c)

: a * c ≤ b * c :=

begin

by_cases h3 : b ≤ a,

{ have h3a : a = b :=

le_antisymm h1 h3,

show a * c ≤ b * c,

by rw h3a },

{ by_cases h4 : c = 0,

{ calc a * c = a * 0 : by rw h4

... = 0 : by rw mul_zero

... ≤ 0 : le_refl 0

... = b * 0 : by rw mul_zero

... = b * c : by {congr ; rw h4}},

{ apply le_of_lt,

apply mul_lt_mul_of_pos_right,

{ show a < b,

by exact lt_of_le_not_le h1 h3 },

{ show 0 < c,

by exact lt_of_le_of_ne h2 (ne.symm h4) }}},

end

-- 3ª demostración

example

(h1 : a ≤ b)

(h2 : 0 ≤ c)

: a * c ≤ b * c :=

-- by library_search

mul_le_mul_of_nonneg_right h1 h2

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.

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

PorJosé A. Alonso 27 octubre 202221 octubre 2022

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

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

PorJosé A. Alonso 26 octubre 202221 octubre 2022

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

   a ≤ b → 0 ≤ b - a

1	a ≤ b → 0 ≤ b - a

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

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

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

import algebra.order.ring

variables {R : Type*} [ordered_ring R]

variables a b : R

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

sorry