Ir al contenido principal

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

Subcategorías:

RSS feed (Foundations, en)

Canal RSS (Fundamentos, es)

También disponible en:

English (Foundations)

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…

Las particiones definen relaciones de equivalencia

Fundamentos/Relaciones de equivalencia

Cada familia de conjuntos \(P\) define una relación de forma que dos elementos están relacionados si algún conjunto de \(P\) contiene a ambos elementos. Se puede definir en Lean4 por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia \(P\) de subconjuntos de \(X\) es una partición de \(X\) si cada elemento de \(X\) pertenece a un único conjunto de \(P\) y todos los elementos de \(P\) son no vacíos. Se puede definir en Lean4 por

   def particion (P : set (set X)) : Prop :=
     (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

Demostrar con Lean4 que si \(P\) es una partición de \(X\), entonces la relación definida por \(P\) es una relación de equivalencia.

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

import Mathlib.Tactic

variable {X : Type}
variable (P : Set (Set X))

def relacion (P : Set (Set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : Set (Set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example
  (h : particion P)
  : Equivalence (relacion P) :=
by sorry

Leer más…

Las particiones definen relaciones transitivas

Fundamentos/Relaciones de equivalencia

Cada familia de conjuntos \(P\) define una relación de forma que dos elementos están relacionados si algún conjunto de \(P\) contiene a ambos elementos. Se puede definir en Lean4 por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia \(P\) de subconjuntos de \(X\) es una partición de \(X\) si cada elemento de \(X\) pertenece a un único conjunto de \(P\) y todos los elementos de \(P\) son no vacíos. Se puede definir en Lean por

   def particion (P : set (set X)) : Prop :=
     (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

Demostrar con Lean4 que si \(P\) es una partición de \(X\), entonces la relación definida por \(P\) es transitiva.

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

import Mathlib.Tactic

variable {X : Type}
variable (P : Set (Set X))

def relacion (P : Set (Set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : Set (Set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example
  (h : particion P)
  : Transitive (relacion P) :=
by sorry

Leer más…

Las familias de conjuntos definen relaciones simétricas

Fundamentos/Relaciones de equivalencia

Cada familia de conjuntos \(P\) define una relación de forma que dos elementos están relacionados si algún conjunto de \(P\) contiene a ambos elementos. Se puede definir en Lean4 por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

Demostrar con Lean4 que si \(P\) es una familia de subconjuntos de \(X\), entonces la relación definida por \(P\) es simétrica.

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

import Mathlib.Tactic

variable {X : Type}
variable (P : Set (Set X))

def relacion (P : Set (Set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

-- 1ª demostración
-- ===============

example : Symmetric (relacion P) :=
by
  intros x y hxy
  -- x y : X
  -- hxy : relacion P x y
  -- ⊢ relacion P y x
  rcases hxy with ⟨A, h1⟩
  -- A : Set X
  -- h1 : A ∈ P ∧ x ∈ A ∧ y ∈ A
  have h2 : A ∈ P ∧ y ∈ A ∧ x ∈ A := by tauto
  exact ⟨A, h2⟩

-- 2ª demostración
-- ===============

example : Symmetric (relacion P) :=
by
  unfold Symmetric
  -- ⊢ ∀ ⦃x y : X⦄, relacion P x y → relacion P y x
  intros x y hxy
  -- x y : X
  -- hxy : relacion P x y
  -- ⊢ relacion P y x
  unfold relacion at *
  -- hxy : ∃ A, A ∈ P ∧ x ∈ A ∧ y ∈ A
  -- ⊢ ∃ A, A ∈ P ∧ y ∈ A ∧ x ∈ A
  rcases hxy with ⟨A, hAP, ⟨hxA, hyA⟩⟩
  -- A : Set X
  -- hAP : A ∈ P
  -- hxA : x ∈ A
  -- hyA : y ∈ A
  use A

-- 3ª demostración
-- ===============

example : Symmetric (relacion P) :=
by
  intros x y hxy
  -- x y : X
  -- hxy : relacion P x y
  -- ⊢ relacion P y x
  rcases hxy with ⟨A, hAP, ⟨hxA, hyA⟩⟩
  -- A : Set X
  -- hAP : A ∈ P
  -- hxA : x ∈ A
  -- hyA : y ∈ A
  use A

-- 4ª demostración
-- ===============

example : Symmetric (relacion P) :=
by
  intros x y hxy
  -- x y : X
  -- hxy : relacion P x y
  -- ⊢ relacion P y x
  rcases hxy with ⟨A, hAP, ⟨hxA, hyA⟩⟩
  -- A : Set X
  -- hAP : A ∈ P
  -- hxA : x ∈ A
  -- hyA : y ∈ A
  exact ⟨A, ⟨hAP, hyA, hxA⟩⟩

Leer más…

Las particiones definen relaciones reflexivas

Fundamentos/Relaciones de equivalencia

Cada familia de conjuntos \(P\) define una relación de forma que dos elementos están relacionados si algún conjunto de \(P\) contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia de subconjuntos de \(X\) es una partición de \(X\) si cada elemento de \(X\) pertenece a un único conjunto de \(P\) y todos los elementos de \(P\) son no vacíos. Se puede definir en Lean por

   def particion (P : set (set X)) : Prop :=
     (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

Demostrar con Lean4 que si \(P\) es una partición de \(X\), entonces la relación definida por \(P\) es reflexiva.

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

import Mathlib.Tactic

variable {X : Type}
variable (P : Set (Set X))

def relacion (P : Set (Set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : Set (Set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example
  (h : particion P)
  : Reflexive (relacion P) :=
by sorry

Leer más…

El conjunto de las clases de equivalencia es una partición

Fundamentos/Relaciones de equivalencia

Demostrar con Lean4 que si \(R\) es una relación de equivalencia en \(X\), entonces las clases de equivalencia de \(R\) es una partición de \(X\).

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

import Mathlib.Tactic

variable {X : Type}
variable {x y: X}
variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

def particion (P : Set (Set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

lemma aux
  (h : Equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
fun _ hz ↦ h.3 hxy hz

example
  (h : Equivalence R)
  : particion {a : Set X | ∃ s : X, a = clase R s} :=
by sorry

Leer más…

Las clases de equivalencia de elementos no relacionados son disjuntas

Fundamentos/Relaciones de equivalencia

Demostrar con Lean4 que las clases de equivalencia de elementos no relacionados son disjuntas.

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

import Mathlib.Tactic

variable {X : Type}
variable {x y: X}
variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

example
  (h : Equivalence R)
  (hxy : ¬ R x y)
  : clase R x ∩ clase R y = ∅ :=
by sorry

Leer más…

Las clases de equivalencia de elementos relacionados son iguales

Fundamentos/Relaciones de equivalencia

Demostrar con Lean4 que las clases de equivalencia de elementos relacionados son iguales.

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

import Mathlib.Tactic

variable {X : Type}
variable {x y: X}
variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

example
  (h : Equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
by sorry

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…