Ir al contenido principal

Publicaciones sobre Funciones (publicaciones antiguas, página 1)

RSS feed (Functions, en)

Canal RSS (Funciones, es)

También disponible en:

English (Functions)

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…

Si g es inyectiva y g ∘ f₁ = g ∘ f₂, entonces f₁ = f₂

Fundamentos/Funciones

Sean \(f_1\) y \(f_2\) funciones de \(X\) en \(Y\) y \(g\) una función de \(Y\) en \(Z\). Demostrar con Lean4 que si \(g\) es inyectiva y \(g ∘ f_1 = g ∘ f_2\), entonces \(f_1 = f_2\).

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

import Mathlib.Tactic
open Function

variable {X Y Z : Type _}
variable {f₁ f₂ : X → Y}
variable {g : Y → Z}

example
  (hg : Injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
by sorry

Leer más…

La equipotencia es una relación transitiva

Fundamentos/Funciones

Dos conjuntos \(A\) y \(B\) son equipotentes (y se denota por \(A ≃ B\)) si existe una aplicación biyectiva entre ellos. La equipotencia se puede definir en Lean4 por

   def es_equipotente (A B : Type _) : Prop :=
     ∃ g : A → B, Bijective g

   local infixr:50 " ⋍ " => es_equipotente

Demostrar con Lean4 que la relación de equipotencia es transitiva.

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

import Mathlib.Tactic
open Function

def es_equipotente (A B : Type _) :=
  ∃ g : A → B, Bijective g

local infixr:50 " ⋍ " => es_equipotente

example : Transitive (. ⋍ .) :=
by sorry

Leer más…

La composición de funciones biyectivas es biyectiva

Fundamentos/Funciones

Demostrar con Lean4 que la composición de dos funciones biyectivas es una función biyectiva.

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

import Mathlib.Tactic
open Function

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

example
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
by sorry

Leer más…

La equipotencia es una relación simétrica

Fundamentos/Funciones

Dos conjuntos \(A\) y \(B\) son equipotentes (y se denota por \(A ≃ B\)) si existe una aplicación biyectiva entre ellos. La equipotencia se puede definir en Lean4 por

   def es_equipotente (A B : Type _) : Prop :=
     ∃ g : A → B, Bijective g

   local infixr:50 " ⋍ " => es_equipotente

Demostrar con Lean4 que la relación de equipotencia es simétrica.

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

import Mathlib.Tactic

open Function

def es_equipotente (A B : Type _) : Prop :=
  ∃ g : A → B, Bijective g

local infixr:50 " ⋍ " => es_equipotente

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

lemma aux1
  (hf : Bijective f)
  : tiene_inversa f :=
by
  cases' (bijective_iff_has_inverse.mp hf) with g hg
  -- g : Y → X
  -- hg : LeftInverse g f ∧ Function.RightInverse g f
  aesop (add norm unfold [tiene_inversa, inversa])

lemma aux2
  (hg : inversa g f)
  : Bijective g :=
by
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  exact ⟨f, hg⟩

example : Symmetric (. ⋍ .) :=
by sorry

Leer más…

La inversa de una función es biyectiva

Fundamentos/Funciones

En Lean4 se puede definir que \(g\) es una inversa de \(f\) por

   def inversa (f : X → Y) (g : Y → X) :=
     (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

Demostrar con Lean4 que si \(g\) es una inversa de \(f\), entonces \(g\) es biyectiva.

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

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)
variable (g : Y → X)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

example
  (hg : inversa g f)
  : Bijective g :=
by sorry

Leer más…

La equipotencia es una relación reflexiva

Fundamentos/Funciones

Dos conjuntos \(A\) y \(B\) son equipotentes (y se denota por \(A ≃ B\)) si existe una aplicación biyectiva entre ellos. La equipotencia se puede definir en Lean por

   def es_equipotente (A B : Type _) : Prop :=
     ∃ g : A → B, Bijective g

   local infixr:50 " ⋍ " => es_equipotente

Demostrar que la relación de equipotencia es reflexiva.

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

import Mathlib.Tactic

open Function

def es_equipotente (A B : Type _) : Prop :=
  ∃ g : A → B, Bijective g

local infixr:50 " ⋍ " => es_equipotente

example : Reflexive (. ⋍ .) :=
by sorry

Leer más…

Las funciones biyectivas tienen inversa

Fundamentos/Funciones

En Lean4 se puede definir que \(g\) es una inversa de \(f\) por

   def inversa (f : X → Y) (g : Y → X) :=
     (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

y que \(f\) tiene inversa por

   def tiene_inversa (f : X → Y) :=
     ∃ g, inversa f g

Demostrar con Lean4 que si la función \(f\) es biyectiva, entonces \(f\) tiene inversa.

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

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

example
  (hf : Bijective f)
  : tiene_inversa f :=
by sorry

Leer más…

Las funciones con inversa son biyectivas

Fundamentos/Funciones

En Lean4 se puede definir que \(g\) es una inversa de \(f\) por

   def inversa (f : X → Y) (g : Y → X) :=
     (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

y que \(f\) tiene inversa por

   def tiene_inversa (f : X → Y) :=
     ∃ g, inversa g f

Demostrar con Lean4 que si la función \(f\) tiene inversa, entonces \(f\) es biyectiva.

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

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

example
  (hf : tiene_inversa f)
  : Bijective f :=
by sorry

Leer más…