Ir al contenido principal

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

RSS feed (Functions, en)

Canal RSS (Funciones, es)

También disponible en:

English (Functions)

Las funciones suprayectivas tienen inversa por la derecha

Fundamentos/Funciones

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

que \(g\) es una inversa por la derecha de \(f\) está definido por

   RightInverse (g : β → α) (f : α → β) : Prop :=
      LeftInverse f g

y que \(f\) tenga inversa por la derecha está definido por

   HasRightInverse (f : α → β) : Prop :=
      ∃ g : β → α, RightInverse g f

Finalmente, que \(f\) es suprayectiva está definido por

   def Surjective (f : α → β) : Prop :=
      ∀ b, ∃ a, f a = b

Demostrar con Lean4 que si \(f\) es una función suprayectiva, entonces \(f\) tiene inversa por la derecha.

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

import Mathlib.Tactic
open Function Classical

variable {α β: Type _}
variable {f : α → β}

example
  (hf : Surjective f)
  : HasRightInverse f :=
by sorry

Leer más…

Las funciones con inversa por la derecha son suprayectivas

Fundamentos/Funciones

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

que \(g\) es una inversa por la derecha de \(f\) está definido por

   RightInverse (g : β → α) (f : α → β) : Prop :=
      LeftInverse f g

y que \(f\) tenga inversa por la derecha está definido por

   HasRightInverse (f : α → β) : Prop :=
      ∃ g : β → α, RightInverse g f

Finalmente, que \(f\) es suprayectiva está definido por

   def Surjective (f : α → β) : Prop :=
      ∀ b, ∃ a, f a = b

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

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

import Mathlib.Tactic
open Function

variable {α β: Type _}
variable {f : α → β}

example
  (hf : HasRightInverse f)
  : Surjective f :=
by sorry

Leer más…

Las funciones inyectivas tienen inversa por la izquierda

Fundamentos/Funciones

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

y que \(f\) tenga inversa por la izquierda está definido por

   HasLeftInverse (f : α → β) : Prop :=
      ∃ finv : β → α, LeftInverse finv f

Finalmente, que \(f\) es inyectiva está definido por

   Injective (f : α → β) : Prop :=
      ∀ ⦃x y⦄, f x = f y → x = y

Demostrar con Lean4 que si \(f\) es una función inyectiva con dominio no vacío, entonces \(f\) tiene inversa por la izquierda.

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

import Mathlib.Tactic

open Function Classical

variable {α β: Type _}
variable {f : α → β}

example
  [hα : Nonempty α]
  (hf : Injective f)
  : HasLeftInverse f :=
by sorry

Leer más…

Si g ∘ f es suprayectiva, entonces g es suprayectiva

Fundamentos/Funciones

Sean \(f: X → Y\) y \(g: Y → Z\). Demostrar que si \(g ∘ f\) es suprayectiva, entonces \(g\) es suprayectiva.

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
  (h : Surjective (g ∘ f))
  : Surjective g :=
by sorry

Leer más…

Si g ∘ f es inyectiva, entonces f es inyectiva

Fundamentos/Funciones

Sean \(f: X → Y\) y \(g: Y → Z\). Demostrar con Lean4 que si \(g ∘ f\) es inyectiva, entonces \(f\) es inyectiva.

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
  (h : Injective (g ∘ f))
  : Injective f :=
by sorry

Leer más…

Las funciones con inversa por la izquierda son inyectivas

Fundamentos/Funciones

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

y que \(f\) tenga inversa por la izquierda está definido por

   HasLeftInverse (f : α → β) : Prop :=
      ∃ finv : β → α, LeftInverse finv f

Finalmente, que \(f\) es inyectiva está definido por

   Injective (f : α → β) : Prop :=
      ∀ ⦃x y⦄, f x = f y → x = y

Demostrar con Lean4 que si \(f\) tiene inversa por la izquierda, entonces \(f\) es inyectiva.

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

import Mathlib.Tactic
open Function

universe u v
variable {α : Type u}
variable {β : Type v}
variable {f : α → β}

example
  (hf : HasLeftInverse f)
  : Injective f :=
by sorry

Leer más…

Teorema de Cantor

Fundamentos/Funciones

Demostrar con Lean4 el teorema de Cantor; es decir, que no existe ninguna aplicación suprayectiva de un conjunto en el conjunto de sus subconjuntos.

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

import Mathlib.Data.Set.Basic

open Function

variable {α : Type}

example : ∀ f : α → Set α, ¬Surjective f :=
by sorry

Leer más…

Imagen inversa de la intersección general

Fundamentos/Funciones

Demostrar con Lean4 que \[ f⁻¹\left[\bigcap_{i \in I} B_i\right] = \bigcap_{i \in I} f⁻¹[B_i] \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
by sorry

Leer más…

Imagen inversa de la unión general

Fundamentos/Funciones

Demostrar con Lean4 que \[ f⁻¹\left[⋃ᵢ Bᵢ\right] = ⋃ᵢ f⁻¹[Bᵢ] \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

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

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=
by sorry

Leer más…

Imagen de la intersección general mediante aplicaciones inyectivas

Fundamentos/Funciones

Demostrar con Lean4 que si \(f\) es inyectiva, entonces \[⋂ᵢf[Aᵢ] ⊆ f\left[⋂ᵢAᵢ\right] \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set Function

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

example
  (i : I)
  (injf : Injective f)
  : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=
by
sorry

Leer más…