octubre 2022 – Calculemus

Si X es un espacio métrico y x, y ∈ X, entonces dist(x,y) ≥ 0

PorJosé A. Alonso 31 octubre 202226 octubre 2022

Demostrar que si X es un espacio métrico y x, y ∈ X, entonces

   0 ≤ dist x y

1	0 ≤ dist x y

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

import topology.metric_space.basic

variables {X : Type*} [metric_space X]
variables x y : X

example : 0 ≤ dist x y :=
sorry

import topology.metric_space.basic

variables {X : Type*} [metric_space X]

variables x y : X

example : 0 ≤ dist x y :=

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

Si R es un retículo tal que x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z), entonces (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)

PorJosé A. Alonso 25 octubre 202221 octubre 2022

Demostrar que Si R es un retículo tal que

   ∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)

1	∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)

entonces

   ∀ a b c : R, (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)

1	∀ a b c : R, (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)

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

import order.lattice
variables {R : Type*} [lattice R]

example
  (h : ∀ x y z : R, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z))
  : ∀ a b c : R, (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) :=
sorry

import order.lattice

variables {R : Type*} [lattice R]

example

(h : ∀ x y z : R, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z))

: ∀ a b c : R, (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) :=

sorry

Si R es un retículo tal que (∀ x y z ∈ R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))), entonces (∀ a b c ∈ R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c))

PorJosé A. Alonso 24 octubre 202220 octubre 2022

Demostrar que si R es un retículo tal que

   (∀ x y z ∈ R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))),

1	(∀ x y z ∈ R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))),

entonces

   (∀ a b c ∈ R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c))

1	(∀ a b c ∈ R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c))

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

import order.lattice
variables {R : Type*} [lattice R]

example
  (h : ∀ x y z : R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))
  : ∀ a b c : R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) :=
sorry

import order.lattice

variables {R : Type*} [lattice R]

example

(h : ∀ x y z : R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))

: ∀ a b c : R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) :=

sorry

Si R es un retículo y x, y ∈ R, entonces x ⊔ (x ⊓ y) = x

PorJosé A. Alonso 21 octubre 202220 octubre 2022

Demostrar que si R es un retículo y x, y ∈ R, entonces

   x ⊔ (x ⊓ y) = x

1	x ⊔ (x ⊓ y) = x

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

import order.lattice
variables {R : Type*} [lattice R]
variables x y : R

example : x ⊔ (x ⊓ y) = x :=
sorry

import order.lattice

variables {R : Type*} [lattice R]

variables x y : R

example : x ⊔ (x ⊓ y) = x :=

sorry

Si R es un retículo y x, y ∈ R, entonces x ⊓ (x ⊔ y) = x

PorJosé A. Alonso 20 octubre 2022

Demostrar que si R es un retículo y x, y ∈ R, entonces

x ⊓ (x ⊔ y) = x

1	x ⊓ (x ⊔ y) = x

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

import order.lattice
variables {R : Type*} [lattice R]
variables x y : R

example : x ⊓ (x ⊔ y) = x :=
sorry

import order.lattice

variables {R : Type*} [lattice R]

variables x y : R

example : x ⊓ (x ⊔ y) = x :=

sorry

Si R es un retículo y x, y, z ∈ R, entonces (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)

PorJosé A. Alonso 20 octubre 2022

Demostrar que si R es un retículo y x, y, z ∈ R, entonces

(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)

1	(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)

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

import order.lattice

variables {R : Type*} [lattice R]
variables x y z : R

example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) :=
sorry

import order.lattice

variables {R : Type*} [lattice R]

variables x y z : R

example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) :=

sorry

Si R es un retículo y x, y, z ∈ R, entonces (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)

PorJosé A. Alonso 18 octubre 2022

Demostrar que si R es un retículo y x, y, z ∈ R, entonces

(x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)

1	(x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)

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

import order.lattice

variables {R : Type*} [lattice R]
variables x y z : R

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
sorry

import order.lattice

variables {R : Type*} [lattice R]

variables x y z : R

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=

sorry