Ir al contenido principal

Monotonía de la imagen inversa

Fundamentos/Funciones

Demostrar con Lean4 y con Isabelle/HOL que si \(u ⊆ v\), entonces \(f⁻¹[u] ⊆ f⁻¹[v]\).

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

import Mathlib.Data.Set.Function
open Set

variable {α β : Type _}
variable (f : α → β)
variable (u v : Set β)

example
  (h : u ⊆ v)
  : f ⁻¹' u ⊆ f ⁻¹' v :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Monotonia_de_la_imagen_inversa
imports Main
begin

lemma
  assumes "u ⊆ v"
  shows "f -` u ⊆ f -` v"
sorry

end

Leer más…

Monotonía de la imagen de conjuntos

Fundamentos/Funciones

Demostrar con Lean4 y con Isabelle/HOL que si \(s ⊆ t\), entonces \(f[s] ⊆ f[t]\).

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Monotonia_de_la_imagen_de_conjuntos
imports Main
begin

lemma
  assumes "s ⊆ t"
  shows "f ` s ⊆ f ` t"
sorry

end

Leer más…

Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]​]

Fundamentos/Funciones

Demostrar con Lean4 y con Isabelle/HOL que si \(f\) es suprayectiva, entonces \[ u ⊆ f[f⁻¹[u]] \]

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

import Mathlib.Data.Set.Function
open Set Function
variable {α β : Type _}
variable (f : α → β)
variable (u : Set β)

example
  (h : Surjective f)
  : u ⊆ f '' (f⁻¹' u) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_imagen_inversa_de_aplicaciones_suprayectivas
imports Main
begin

lemma
  assumes "surj f"
  shows "u ⊆ f ` (f -` u)"
sorry

end

Leer más…

Demostraciones de "f[f⁻¹[u]] ⊆ u"

Fundamentos/Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ f[f⁻¹[u]] ⊆ u \]

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

import Mathlib.Data.Set.Function
open Set

variable {α β : Type _}
variable (f : α → β)
variable (u : Set β)

example : f '' (f⁻¹' u) ⊆ u :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_imagen_inversa
imports Main
begin

lemma "f ` (f -` u) ⊆ u"
sorry

end

Leer más…

Asociatividad de la concatenación de listas

Estructuras discretas/Listas

En Lean4 la operación de concatenación de listas se representa por (++) y está caracterizada por los siguientes lemas

nil_append  : [] ++ ys = ys
cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

Demostrar que la concatenación es asociativa; es decir,

xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

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

import Mathlib.Data.List.Basic
open List

variable {α : Type}
variable (xs ys zs : List α)

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

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction' xs with a as HI
  . calc [] ++ (ys ++ zs)
         = ys ++ zs                := nil_append (ys ++ zs)
       _ = ([] ++ ys) ++ zs        := congrArg (. ++ zs) (nil_append ys).symm
  . calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) := cons_append a as (ys ++ zs)
       _ = a :: ((as ++ ys) ++ zs) := congrArg (a :: .) HI
       _ = (a :: (as ++ ys)) ++ zs := (cons_append a (as ++ ys) zs).symm

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

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction' xs with a as HI
  . calc [] ++ (ys ++ zs)
         = ys ++ zs                := by rw [nil_append]
       _ = ([] ++ ys) ++ zs        := by rw [nil_append]
  . calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) := by rw [cons_append]
       _ = a :: ((as ++ ys) ++ zs) := by rw [HI]
       _ = (a :: (as ++ ys)) ++ zs := by rw [cons_append]
       _ = ((a :: as) ++ ys) ++ zs := by rw [← cons_append]

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

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction' xs with a as HI
  . calc [] ++ (ys ++ zs)
         = ys ++ zs                := by exact rfl
       _ = ([] ++ ys) ++ zs        := by exact rfl
  . calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) := rfl
       _ = a :: ((as ++ ys) ++ zs) := by rw [HI]
       _ = (a :: (as ++ ys)) ++ zs := rfl
       _ = ((a :: as) ++ ys) ++ zs := rfl

-- 4ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction' xs with a as HI
  . calc [] ++ (ys ++ zs)
         = ys ++ zs                := by simp
       _ = ([] ++ ys) ++ zs        := by simp
  . calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) := by simp
       _ = a :: ((as ++ ys) ++ zs) := congrArg (a :: .) HI
       _ = (a :: (as ++ ys)) ++ zs := by simp
       _ = ((a :: as) ++ ys) ++ zs := by simp

-- 5ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction' xs with a as
  . simp
  . exact (append_assoc (a :: as) ys zs).symm

-- 6ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction' xs with a as HI
  . -- ⊢ [] ++ (ys ++ zs) = ([] ++ ys) ++ zs
    rw [nil_append]
    -- ⊢ ys ++ zs = ([] ++ ys) ++ zs
    rw [nil_append]
  . -- a : α
    -- as : List α
    -- HI : as ++ (ys ++ zs) = as ++ ys ++ zs
    -- ⊢ (a :: as) ++ (ys ++ zs) = ((a :: as) ++ ys) ++ zs
    rw [cons_append]
    -- ⊢ a :: (as ++ (ys ++ zs)) = ((a :: as) ++ ys) ++ zs
    rw [HI]
    -- ⊢ a :: ((as ++ ys) ++ zs) = ((a :: as) ++ ys) ++ zs
    rw [cons_append]
    -- ⊢ a :: ((as ++ ys) ++ zs) = (a :: (as ++ ys)) ++ zs
    rw [cons_append]

-- 7ª demostración
-- ===============

lemma conc_asoc_1 (xs ys zs : List α) :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction xs with
  | nil => calc
    [] ++ (ys ++ zs)
        = ys ++ zs         := by rw [nil_append]
      _ = ([] ++ ys) ++ zs := by rw [nil_append]
  | cons a as HI => calc
    (a :: as) ++ (ys ++ zs)
        = a :: (as ++ (ys ++ zs)) := by rw [cons_append]
      _ = a :: ((as ++ ys) ++ zs) := by rw [HI]
      _ = (a :: (as ++ ys)) ++ zs := by rw [cons_append]
      _ = ((a :: as) ++ ys) ++ zs := congrArg (. ++ zs) (cons_append a as ys)

-- 8ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs  :=
(append_assoc xs ys zs).symm

-- 9ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by simp

-- Lemas usados
-- ============

-- variable (x : α)
-- #check (append_assoc xs ys zs : (xs ++ ys) ++ zs = xs ++ (ys ++ zs))
-- #check (cons_append x xs ys : (x :: xs) ++ ys = x :: (xs ++ ys))
-- #check (cons_inj x : x :: xs = x :: ys ↔ xs = ys)
-- #check (nil_append xs : [] ++ xs = xs)

Leer más…

Pruebas de length (replicate n x) = n

Estructuras discretas/Listas

En Lean4 están definidas las funciones length y replicate tales que

  • (length xs) es la longitud de la lista xs. Por ejemplo,

    length [1,2,5,2] = 4

  • (replicate n x) es la lista que tiene el elemento x n veces. Por ejemplo,

    replicate 3 7 = [7, 7, 7]

Demostrar que

length (replicate n x) = n

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

import Mathlib.Data.List.Basic
open Nat
open List

variable {α : Type}
variable (x : α)
variable (n : ℕ)

example :
  length (replicate n x) = n :=
by sorry

Leer más…

Si u es una sucesión no decreciente y su límite es a, entonces u(n) ≤ a para todo n

Análisis/Límites

En Lean4, una sucesión \(u_0, u_1, u_2, ...\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es \(u_n\).

En Lean4, se define que \(a\) es el límite de la sucesión \(u\), por

   def limite (u: ℕ → ℝ) (a: ℝ) :=
     ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

y que la sucesión \(u\) es no decreciente por

   def no_decreciente (u : ℕ → ℝ) :=
     ∀ n m, n ≤ m → u n ≤ u m

Demostrar con Lean4 que si \(u\) es una sucesión no decreciente y su límite es \(a\), entonces \(u(n) ≤ a\) para todo \(n\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {u : ℕ → ℝ}
variable (a : ℝ)

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε

def no_decreciente (u : ℕ → ℝ) :=
  ∀ n m, n ≤ m → u n ≤ u m

example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
by sorry

Leer más…

Las sucesiones divergentes positivas no tienen límites finitos

Análisis/Límites

En Lean4, una sucesión \(u_0, u_1, u_2, ...\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es \(uₙ\).

Se define que \(a\) es el límite de la sucesión \(u\), por

   def limite (u: ℕ → ℝ) (a: ℝ) :=
     ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

La sucesión \(u\) diverge positivamente cuando, para cada número real \(A\), se puede encontrar un número natural \(m\) tal que si \(n ≥ m\), entonces \(uₙ > A\). En Lean se puede definir por

   def diverge_positivamente (u : ℕ → ℝ) :=
     ∀ A, ∃ m, ∀ n ≥ m, u n > A

Demostrar que si \(u\) diverge positivamente, entonces ningún número real es límite de \(u\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {u : ℕ → ℝ}

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε

def diverge_positivamente (u : ℕ → ℝ) :=
  ∀ A, ∃ m, ∀ n ≥ m, u n > A

example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
by sorry

Leer más…

Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u

Análisis/Límites

En Lean4, una sucesión \(u_0, u_1, u_2, u_3 ...\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es el término \(u_n\).

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \(u_0, u_2, u_4, u_6, ...\) se ha obtenido con la función de extracción \(f\) tal que \(f(n) = 2n\).

En Lean4, se puede definir que \(f\) es una función de extracción por

   def extraccion (f : ℕ → ℕ) :=
     ∀ n m, n < m → f n < f m

que a es un límite de u por

   def limite (u : ℕ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

que a es un punto de acumulación de u por

   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
     ∃ f, extraccion f ∧ limite (u ∘ f) a

que la sucesión u es de Cauchy por

   def suc_cauchy (u : ℕ → ℝ) :=
     ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε

Demostrar con Lean4 que si \(u\) es una sucesión de Cauchy y \(a\) es un punto de acumulación de \(u\), entonces \(a\) es el límite de \(u\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

open Nat

variable {u : ℕ → ℝ}
variable {a : ℝ}

example
  (hu : suc_cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
by sorry

Leer más…

El punto de acumulación de las sucesiones convergente es su límite

Análisis/Límites

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \[ u_0, u_2, u_4, u_6, ... \] se ha obtenido con la función de extracción \(f\) tal que \(f(n) = 2n\).

En Lean4, se puede definir que \(f\) es una función de extracción por

   def extraccion (f : ℕ → ℕ) :=
     ∀ n m, n < m → f n < f m

que \(a\) es un límite de \(u\) por

   def limite (u : ℕ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

que \(u\) es convergente por

   def convergente (u : ℕ → ℝ) :=
     ∃ a, limite u a

que \(a\) es un punto de acumulación de \(u\) por

   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
     ∃ f, extraccion f ∧ limite (u ∘ f) a

Demostrar con Lean4 que si \(u\) es una sucesión convergente y \(a\) es un punto de acumulación de \(u\), entonces \(a\) es un límite de \(u\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

open Nat

variable {u : ℕ → ℝ}
variable {a : ℝ}

def extraccion (f : ℕ → ℕ) :=
  ∀ n m, n < m → f n < f m

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
  ∃ f, extraccion f ∧ limite (u ∘ f) a

example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
by sorry

Leer más…