Skip to main content

Monotonía de la imagen de conjuntos

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

Read more…

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

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

Read more…

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

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

Read more…

Nicomachus’s theorem

Induction

Prove the Nicomachus's theorem which states that the sum of the cubes of the first \(n\) natural numbers is equal to the square of the sum of the first \(n\) natural numbers; that is, for any natural number n we have \[ 1^3 + 2^3 + ... + n^3 = (1 + 2 + ... + n)^2 \]

To do this, complete the following Lean4 theory:

import Mathlib.Data.Nat.Defs
import Mathlib.Tactic

open Nat

variable ( n : ℕ)

def sum : ℕ → ℕ
  | 0      => 0
  | succ n => sum n + (n+1)

def sumCubes : ℕ → ℕ
  | 0   => 0
  | n+1 => sumCubes n + (n+1)^3

example :
  sumCubes n = (sum n)^2 :=
by sorry

Read more…

If uₙ tends to a y vₙ tends to b, then uₙvₙ tends to ab

Limits

In Lean4, a sequence \(u_0, u_1, u_2, ...\) can be represented by a function \(u : ℕ → ℝ\) such that \(u(n)\) is \(u_n\).

It is defined that the sequence \(u\) tends to \(c\) by:

   def TendsTo (u : ℕ → ℝ) (c : ℝ) :=
     ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

Prove that if \(u_n\) tends to \(a\) and \(v_n\) tends to \(b\), then \(u_nv_n\) tends to \(ab\).

To do this, complete the following Lean4 theory:

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

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

def TendsTo (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

example
  (hu : TendsTo u a)
  (hv : TendsTo v b)
  : TendsTo (fun n ↦ u n * v n) (a * b) :=
by sorry

Read more…

If the limit of the sequence u(n) is a and c ∈ ℝ, then the limit of u(n)c is ac

Limits

In Lean, a sequence \(u_₀, u_₁, u_₂, ... \) can be represented by a function \(u : ℕ → ℝ\) such that \(u(n)\) is \(u_n\).

It is defined that \(a\) is the limit of the sequence \(u\), by

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

Prove that if the limit of \(u_n\) is \(a\), then the limit of \(u_nc\) is \(ac\).

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

variable (u : ℕ → ℝ)
variable (a c : ℝ)

def TendsTo : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  (h : TendsTo u a)
  : TendsTo (fun n ↦ (u n) * c) (a * c) :=
by sorry

Read more…

If u(n) tends to a, then 7u(n) tends to 7a

Limits

In Lean, a sequence \(u_0, u_1, u_2, ...\) can be represented by a function \(u : ℕ → ℝ\) such that \(u(n)\) is the term \(u_n\).

We define that \(u\) tends to \(a\) by

   def tendsTo : (ℕ → ℝ) → ℝ → Prop :=
     fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

Prove that if \(u_n\) tends to \(a\), then \(7u\_n\) tends to \(7a\).

To do this, complete the following Lean4 theory:

import Mathlib.Tactic

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

def tendsTo : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  (h : tendsTo u a)
  : tendsTo (fun n ↦ 7 * u n) (7 * a) :=
by sorry

Read more…

Pigeonhole principle

Finite sets

Prove the pigeonhole principle; that is, if \(S\) is a finite set and \(T\) and \(U\) are subsets of \(S\) such that the number of elements of \(S\) is less than the sum of the number of elements of \(T\) and \(U\), then the intersection of \(T\) and \(U\) is non-empty.

To do this, complete the following Lean4 theory:

import Mathlib.Data.Finset.Card

open Finset

variable [DecidableEq α]
variable {s t u : Finset α}

set_option pp.fieldNotation false

example
  (hts : t ⊆ s)
  (hus : u ⊆ s)
  (hstu : card s < card t + card u)
  : Finset.Nonempty (t ∩ u) :=
by sorry

Read more…

If f ∘ f is bijective, then f is bijective

Functions

Prove that if \(f ∘ f\) is bijective, then \(f\) is bijective.

To do this, complete the following Lean4 theory:

import Mathlib.Tactic
open Function

variable {X Y Z : Type}
variable  {f : X → Y}
variable  {g : Y → Z}

example
  (f : X → X)
  (h : Bijective (f ∘ f))
  : Bijective f :=
by sorry

Read more…