Teoría de conjuntos

Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s

PorJosé A. Alonso 23 octubre 202318 octubre 2023

Demostrar con Lean4 que si \(a\) es una cota superior de \(s\) y \(a ≤ b\), entonces \(b\) es una cota superior de \(s\).

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

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable (s : Set α)
variable (a b : α)

-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.
def CotaSupConj (s : Set α) (a : α) :=
  ∀ {x}, x ∈ s → x ≤ a

example
  (h1 : CotaSupConj s a)
  (h2 : a ≤ b)
  : CotaSupConj s b :=
by sorry

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]

variable (s : Set α)

variable (a b : α)

-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.

def CotaSupConj (s : Set α) (a : α) :=

∀ {x}, x ∈ s → x ≤ a

example

(h1 : CotaSupConj s a)

(h2 : a ≤ b)

: CotaSupConj s b :=

by sorry

Si r ⊆ s y s ⊆ t, entonces r ⊆ t

PorJosé A. Alonso 20 octubre 202317 octubre 2023

Demostrar con Lean4 que si \(r ⊆ s\) y \(s ⊆ t\), entonces \(r ⊆ t\).

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

import Mathlib.Tactic

open Set

variable {α : Type _}
variable (r s t : Set α)

example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
by sorry

import Mathlib.Tactic

open Set

variable {α : Type _}

variable (r s t : Set α)

example

(rs : r ⊆ s)

(st : s ⊆ t)

: r ⊆ t :=

by sorry

Para cualquier conjunto s, s ⊆ s

PorJosé A. Alonso 19 octubre 202317 octubre 2023

Demostrar con Lean4 que para cualquier conjunto \(s\), \(s ⊆ s\).

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

import Mathlib.Tactic

variable {α : Type _}
variable (s : Set α)

example : s ⊆ s :=
by sorry

import Mathlib.Tactic

variable {α : Type _}

variable (s : Set α)

example : s ⊆ s :=

by sorry

Si f·f es biyectiva, entonces f es biyectiva

PorJosé A. Alonso 28 junio 202228 junio 2022

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

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.

PorJosé A. Alonso 22 junio 202222 junio 2022

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

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

PorJosé A. Alonso 6 mayo 20226 mayo 2022

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

import data.set.basic

open function

variables {α : Type}

example : ∀ f : α → set α, ¬ surjective f :=

sorry

Imagen de la unión

PorJosé A. Alonso 3 mayo 20224 mayo 2022

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

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

PorJosé A. Alonso 30 abril 20221 mayo 2022

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

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

PorJosé A. Alonso 28 abril 202228 abril 2022

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

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

PorJosé A. Alonso 26 abril 202226 abril 2022

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

import data.set.basic

open set

variable {α : Type}

variables s t : set α

example : s ∩ (s ∪ t) = s :=

sorry

Read More «Intersección con su unión»