Menu Close

DAO: La semana en Calculemus (27 de noviembre de 2022)

Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:

A continuación se muestran las soluciones.

1. Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s

Demostrar que si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s

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

import tactic
 
variables {α : Type*} [partial_order α]
variables s : set α
variables a b : α
 
-- (cota_superior s a) expresa que a es una cota superior de s.
def cota_superior (s : set α) (a : α) :=  {x}, x ∈ s  x  a
 
example
  (h1 : cota_superior s a)
  (h2 : a  b)
  : cota_superior s b :=
sorry

Soluciones con Lean

import tactic
 
variables {α : Type*} [partial_order α]
variables s : set α
variables a b : α
 
-- (cota_superior s a) expresa que a es una cota superior de s.
def cota_superior (s : set α) (a : α) :=  {x}, x ∈ s  x  a
 
-- 1ª demostración
-- ===============
 
example
  (h1 : cota_superior s a)
  (h2 : a  b)
  : cota_superior s b :=
begin
  intro x,
  assume xs : x ∈ s,
  have h3 : x  a := h1 xs,
  show x  b,
    by exact le_trans h3 h2,
end
 
-- 2ª demostración
-- ===============
 
example
  (h1 : cota_superior s a)
  (h2 : a  b)
  : cota_superior s b :=
begin
  intros x xs,
  calc x  a : h1 xs
     ...  b : h2
end

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

Referencias

2. Para todo c ∈ ℝ, la función f(x) = x+c es inyectiva

Demostrar que para todo c ∈ ℝ, la función f(x) = x+c es inyectiva.

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

import data.real.basic
 
open function
 
variable {c : }
 
example : injective (λ x, x + c) :=
sorry

Soluciones con Lean

import data.real.basic
 
open function
variable {c : }
 
-- 1ª demostración
-- ===============
 
example : injective (λ x, x + c) :=
begin
  assume x1 : ,
  assume x2 : ,
  assume h1 : (λ x, x + c) x1 = (λ x, x + c) x2,
  have h2 : x1 + c = x2 + c := h1,
  show x1 = x2,
    by exact (add_left_inj c).mp h2,
end
 
-- 2ª demostración
-- ===============
 
example : injective (λ x, x + c) :=
begin
  intros x1 x2 h,
  change x1 + c = x2 + c at h,
  apply add_right_cancel h,
end
 
-- 3ª demostración
-- ===============
 
example : injective (λ x, x + c) :=
begin
  intros x1 x2 h,
  apply (add_left_inj c).mp,
  exact h,
end
 
-- 4ª demostración
-- ===============
 
example : injective (λ x, x + c) :=
λ x1 x2 h, (add_left_inj c).mp h

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

Referencias

3. Para todo c ∈ ℝ-{0}, la función f(x) = x * c es inyectiva

Demostrar que para todo c ∈ ℝ-{0}, la función f(x) = x * c es inyectiva

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

import data.real.basic
 
open function
 
variable {c : }
 
example
  (h : c  0)
  : injective (λ x, c * x) :=
sorry

Soluciones con Lean

import data.real.basic
 
open function
 
variable {c : }
 
-- 1ª demostración
-- ===============
 
example
  (h : c  0)
  : injective (λ x, c * x) :=
begin
  assume x1 : ,
  assume x2 : ,
  assume h1 : (λ x, c * x) x1 = (λ x, c * x) x2,
  have h2 : c * x1 = c * x2 := h1,
  show x1 = x2,
    by exact (mul_right_inj' h).mp h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (h : c  0)
  : injective (λ x, c * x) :=
begin
  intros x1 x2 h',
  dsimp at h',
  apply mul_left_cancel₀ h,
  exact h',
end
 
-- 3ª demostración
-- ===============
 
example
  (h : c  0)
  : injective (λ x, c * x) :=
begin
  intros x1 x2 h',
  dsimp at h',
  exact (mul_right_inj' h).mp h'
end
 
-- 3ª demostración
-- ===============
 
example
  {c : }
  (h : c  0)
  : injective (λ x, c * x) :=
λ x1 x2 h', mul_left_cancel₀ h h'

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

Referencias

4. Si f: A → B y g: B → C son inyectiva, entonces g ∘ f es inyectiva

Demostrar que si f: A → B y g: B → C son inyectiva, entonces g ∘ f es inyectiva.

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

import tactic
 
open function
 
variables {A : Type*} {B : Type*} {C : Type*}
variables {f : A  B} {g : B  C}
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g  f) :=
sorry

Soluciones con Lean

import tactic
 
open function
 
variables {A : Type*} {B : Type*} {C : Type*}
variables {f : A  B} {g : B  C}
 
-- 1ª demostración
-- ===============
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g  f) :=
begin
  assume x : A,
  assume y : A,
  assume h1: (g  f) x = (g  f) y,
  have h2: g (f x) = g (f y) := h1,
  have h3: f x = f y := hg h2,
  show x = y,
    by exact hf h3,
end
 
-- 2ª demostración
-- ===============
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g  f) :=
begin
  intros x y h,
  apply hf,
  apply hg,
  apply h,
end
 
-- 3ª demostración
-- ===============
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g  f) :=
λ x y h, hf (hg h)
 
-- 4ª demostración
-- ===============
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g  f) :=
-- by library_search
injective.comp hg hf
 
-- 5ª demostración
-- ===============
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g  f) :=
-- by hint
by tauto

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

Referencias

5. ∃ x ∈ ℝ, 2 < x < 3

Demostrar que ∃ x ∈ ℝ, 2 < x < 3

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

import data.real.basic
 
example :  x : , 2 < x  x < 3 :=
sorry

Soluciones con Lean

import data.real.basic
 
-- 1ª demostración
-- ===============
 
example :  x : , 2 < x  x < 3 :=
begin
  have h : 2 < (5 : ) / 2  (5 : ) / 2 < 3,
    by norm_num,
  show  x : , 2 < x  x < 3,
    by exact Exists.intro (5 / 2) h,
end
 
-- 2ª demostración
-- ===============
 
example :  x : , 2 < x  x < 3 :=
begin
  have h : 2 < (5 : ) / 2  (5 : ) / 2 < 3,
    by norm_num,
  show  x : , 2 < x  x < 3,
    by exact ⟨5 / 2, h⟩,
end
 
-- 3ª demostración
-- ===============
 
example :  x : , 2 < x  x < 3 :=
begin
  use 5 / 2,
  norm_num
end
 
-- 4ª demostración
-- ===============
 
example :  x : , 2 < x  x < 3 :=5 / 2, by norm_num⟩

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

Referencias

ForMatUS