Menu Close

Etiqueta: Teoría de conjuntos

Si f·f es biyectiva, entonces f es biyectiva

Demostrar que si f·f es biyectiva, entonces f es biyectiva.

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

import tactic
open function
 
variable {X: Type}
 
example
  (f : X  X)
  (Hff : bijective (f  f))
  : bijective f :=
sorry

Si g·f es inyectiva, entonces f es inyectiva.

Demostrar que si g·f es inyectiva, entonces f es inyectiva.

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

import tactic
open function
 
variables {X Y Z : Type}
variable  {f : X  Y}
variable  {g : Y  Z}
 
example
  (Hgf : injective (g  f))
  : injective f :=
sorry

Teorema de Cantor

Demostrar el teorema de Cantor; es decir, que no existe ninguna aplicación suprayectiva de un conjunto en su conjunto potencia.

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

import data.set.basic
open function
 
variables {α : Type}
 
example :  f : α  set α, ¬ surjective f :=
sorry

Imagen de la unión

En Lean, la imagen de un conjunto s por una función f se representa por f '' s; es decir, f '' s = {y | ∃ x, x ∈ s ∧ f x = y}

Demostrar que f '' (s ∪ t) = f '' s ∪ f '' t

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

import data.set.basic
import tactic
 
open set
 
variables {α : Type*} {β : Type*}
variable  f : α  β
variables s t : set α
 
example : f '' (s ∪ t) = f '' s ∪ f '' t :=
sorry

Imagen inversa de la intersección

En Lean, la imagen inversa de un conjunto s (de elementos de tipo por la función f (de tipo α → β) es el conjunto f ⁻¹' s de elementos x (de tipo α) tales que f x ∈ s.

Demostrar que f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v

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

import data.set.basic
 
open set
 
variables {α : Type*} {β : Type*}
variable  f : α  β
variables u v : set β
 
example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=
sorry

Distributiva de la intersección respecto de la unión general

Demostrar que s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s)

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

import data.set.basic
import data.set.lattice
import tactic
 
open set
 
variable {α : Type}
variable s : set α
variable A :   set α
 
example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
sorry

Intersección con su unión

Demostrar que s ∩ (s ∪ t) = s

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

import data.set.basic
open set
 
variable {α : Type}
variables s t : set α
 
example : s ∩ (s ∪ t) = s :=
sorry

Diferencia de diferencia de conjuntos

Demostrar que (s \ t) \ u ⊆ s \ (t ∪ u)

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

import data.set.basic
open set
 
variable {α : Type}
variables s t u : set α
 
example : (s \ t) \ u ⊆ s \ (t ∪ u) :=
sorry

Propiedad semidistributiva de la intersección sobre la unión

Demostrar que s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u).

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

import data.set.basic
open set
 
variable {α : Type}
variables s t u : set α
 
example :
  s ∩ (t ∪ u)(s ∩ t)(s ∩ u) :=
sorry

Propiedad de monotonía de la intersección

Demostrar que la intersección es monótona por la izquierda; es decir, si s ⊆ t, entonces s ∩ u ⊆ t ∩ u.

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

import data.set.basic
open set
 
variable {α : Type}
variables s t u : set α
 
example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
sorry