Skip to main content

Demostraciones de "f[s] \ f[t] ⊆ f[s \ t]"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[f[s] \setminus f[t] ⊆ f[s \setminus 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 : f '' s \ f '' t ⊆ f '' (s \ t) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_diferencia_de_conjuntos
imports Main
begin

lemma "f ` s - f ` t ⊆ f ` (s - t)"
sorry

end

Read more…

Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]

Funciones

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

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

import Mathlib.Data.Set.Function

open Set Function

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

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

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_interseccion_de_aplicaciones_inyectivas
imports Main
begin

lemma
  assumes "inj f"
  shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"
sorry

end

Read more…

Demostraciones de "f[s ∩ t] ⊆ f[s] ∩ f[t]​"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s ∩ t] ⊆ 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 : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_interseccion
imports Main
begin

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"
sorry

end

Read more…

Demostraciones de "f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]​"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]\]

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

import Mathlib.Data.Set.Function

open Set

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

example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B :=
by sorry

y la siguiente teoría de IsabelleHOL:

theory Imagen_inversa_de_la_union
imports Main
begin

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"
sorry

end

Read more…

Monotonía de la imagen inversa

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

Read more…

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…