ForMatUS – Página 16

ForMatUS: Pruebas en Lean de (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j)

PorJosé A. Alonso 30 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 2 pruebas en Lean de la propiedad

(⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j)

1	(⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j)

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Ej. 1. Demostrar
--    (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j)
-- ----------------------------------------------------

import data.set

open set

variables {I J U : Type}
variables (A : I → J → set U)

-- 1ª demostración
example : (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j) :=
begin
  intros x h,
  rw mem_Union at h,
  cases h with i hi,
  rw mem_Inter at hi,
  apply mem_Inter.mpr,
  intro j,
  apply mem_Union.mpr,
  use i,
  exact (hi j),
end

-- 2ª demostración
example : (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j) :=
begin
  intros x h,
  simp * at *,
  cases h with i hi,
  intro j,
  use i,
  exact (hi j),
end

-- ----------------------------------------------------

-- Ej. 1. Demostrar

-- (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j)

-- ----------------------------------------------------

import data.set

open set

variables {I J U : Type}

variables (A : I → J → set U)

-- 1ª demostración

example : (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j) :=

begin

intros x h,

rw mem_Union at h,

cases h with i hi,

rw mem_Inter at hi,

apply mem_Inter.mpr,

intro j,

apply mem_Union.mpr,

use i,

exact (hi j),

end

-- 2ª demostración

example : (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j) :=

begin

intros x h,

simp * at *,

cases h with i hi,

intro j,

use i,

exact (hi j),

end

ForMatUS: Pruebas en Lean de la intersección sobre unión general: C ∩ (⋃i, A i) = (⋃ i, C ∩ A i)

PorJosé A. Alonso 30 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de la propiedad

C ∩ (⋃i, A i) = (⋃ i, C ∩ A i)

1	C ∩ (⋃i, A i) = (⋃ i, C ∩ A i)

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.set

open set

variables {I U : Type}
variables {A : I → set U}
variable  {C : set U}

-- ----------------------------------------------------
-- Ej. 1. Demostrar
--    C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i)
-- ----------------------------------------------------

-- 1ª demostración
example :
  C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i)  :=
begin
  rintros x ⟨hC, hU⟩,
  rw mem_Union at hU,
  cases hU with i hA,
  apply mem_Union.mpr,
  use i,
  split,
  assumption',
end

-- 2ª demostración
example :
  C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i)  :=
begin
  intros x h,
  simp * at *,
end

-- 3ª demostración
lemma inter_Uni_l1 :
  C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i)  :=
by {intros x h, simp * at *}

-- ----------------------------------------------------
-- Ej. 2. Demostrar
--    (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i)
-- ----------------------------------------------------

-- 1ª demostración
example :
  (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=
begin
  intros x h,
  rw mem_Union at h,
  cases h with i hi,
  cases hi with hC hA,
  split,
  { exact hC, },
  { apply mem_Union.mpr,
    use i,
    exact hA, },
end

-- 2ª demostración
example : (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=
begin
  intros x h,
  rw mem_Union at h,
  rcases h with ⟨i, hC, hA⟩,
  split,
  { exact hC, },
  { apply mem_Union.mpr,
    use i,
    exact hA, },
end

-- 3ª demostración
example :
  (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=
begin
  intros x h,
  simp * at *,
end

-- 4ª demostración
lemma inter_Uni_l2 :
  (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=
by {intros x h, simp * at *}

-- ----------------------------------------------------
-- Ej. 3. Demostrar
--    C ∩ (⋃i, A i) = (⋃ i, C ∩ A i)
-- ----------------------------------------------------

-- 1ª demostración
example :
  C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=
eq_of_subset_of_subset inter_Uni_l1 inter_Uni_l2

-- 2ª demostración
example :
  C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=
-- by library_search
inter_Union C A

-- 3ª demostración
example :
  C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=
ext $ by simp

-- 4ª demostración
example :
  C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=
by {ext, simp}

100

101

102

103

104

105

106

107

108

109

110

import data.set

open set

variables {I U : Type}

variables {A : I → set U}

variable {C : set U}

-- ----------------------------------------------------

-- Ej. 1. Demostrar

-- C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i)

-- ----------------------------------------------------

-- 1ª demostración

example :

C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i) :=

begin

rintros x ⟨hC, hU⟩,

rw mem_Union at hU,

cases hU with i hA,

apply mem_Union.mpr,

use i,

split,

assumption',

end

-- 2ª demostración

example :

C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i) :=

begin

intros x h,

simp * at *,

end

-- 3ª demostración

lemma inter_Uni_l1 :

C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i) :=

by {intros x h, simp * at *}

-- ----------------------------------------------------

-- Ej. 2. Demostrar

-- (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i)

-- ----------------------------------------------------

-- 1ª demostración

example :

(⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=

begin

intros x h,

rw mem_Union at h,

cases h with i hi,

cases hi with hC hA,

split,

{ exact hC, },

{ apply mem_Union.mpr,

use i,

exact hA, },

end

-- 2ª demostración

example : (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=

begin

intros x h,

rw mem_Union at h,

rcases h with ⟨i, hC, hA⟩,

split,

{ exact hC, },

{ apply mem_Union.mpr,

use i,

exact hA, },

end

-- 3ª demostración

example :

(⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=

begin

intros x h,

simp * at *,

end

-- 4ª demostración

lemma inter_Uni_l2 :

(⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=

by {intros x h, simp * at *}

-- ----------------------------------------------------

-- Ej. 3. Demostrar

-- C ∩ (⋃i, A i) = (⋃ i, C ∩ A i)

-- ----------------------------------------------------

-- 1ª demostración

example :

C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=

eq_of_subset_of_subset inter_Uni_l1 inter_Uni_l2

-- 2ª demostración

example :

C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=

-- by library_search

inter_Union C A

-- 3ª demostración

example :

C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=

ext $ by simp

-- 4ª demostración

example :

C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=

by {ext, simp}

ForMatUS: Pruebas en Lean de la distributiva de la intersección general sobre la intersección

PorJosé A. Alonso 29 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 4 pruebas en Lean de la propiedad distributiva de la intersección general sobre la intersección :

(⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)

1	(⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Ej. 1. Demostrar
--    (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)
-- ----------------------------------------------------

import data.set
import tactic

open set

variables {I U : Type}
variables {A B : I → set U}

-- 1ª demostración
example :
  (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
begin
  ext,
  split,
  { intro h,
    rw mem_Inter at h,
    split,
    { rw mem_Inter,
      intro i,
      exact (h i).left, },
    { rw mem_Inter,
      intro i,
      exact (h i).right, }},
  { rintro ⟨h1, h2⟩,
    rw mem_Inter at *,
    intro i,
    exact ⟨h1 i, h2 i⟩, },
end

-- 2ª demostración
example :
  (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
ext $
assume x : U,
iff.intro
( assume h : x ∈ ⋂ i, A i ∩ B i,
  have h1 : ∀ i, x ∈ A i ∩ B i,
    from mem_Inter.mp h,
  have h2 : ∀ i, x ∈ A i,
    from assume i, and.left (h1 i),
  have h3 : ∀ i, x ∈ B i,
    from assume i, and.right (h1 i),
  have h4 : x ∈ ⋂ i, A i,
    from mem_Inter.mpr h2,
  have h5 : x ∈ ⋂ i, B i,
    from mem_Inter.mpr h3,
  show x ∈ (⋂ i, A i) ∩ (⋂ i, B i),
    from and.intro h4 h5)
( assume h : x ∈ (⋂ i, A i) ∩ (⋂ i, B i),
  have h1 : ∀ i, x ∈ A i,
    from mem_Inter.mp (and.left h),
  have h2 : ∀ i, x ∈ B i,
    from mem_Inter.mp (and.right h),
  have h3 : ∀ i, x ∈ A i ∩ B i,
    from assume i, and.intro (h1 i) (h2 i),
  show x ∈ ⋂ i, A i ∩ B i,
    from mem_Inter.mpr h3)

-- 3ª demostración
example :
  (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
-- by library_search
Inter_inter_distrib A B

-- 4ª demostración
example :
  (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
ext (by finish)

-- ----------------------------------------------------

-- Ej. 1. Demostrar

-- (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)

-- ----------------------------------------------------

import data.set

import tactic

open set

variables {I U : Type}

variables {A B : I → set U}

-- 1ª demostración

example :

(⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=

begin

ext,

split,

{ intro h,

rw mem_Inter at h,

split,

{ rw mem_Inter,

intro i,

exact (h i).left, },

{ rw mem_Inter,

intro i,

exact (h i).right, }},

{ rintro ⟨h1, h2⟩,

rw mem_Inter at *,

intro i,

exact ⟨h1 i, h2 i⟩, },

end

-- 2ª demostración

example :

(⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=

ext $

assume x : U,

iff.intro

( assume h : x ∈ ⋂ i, A i ∩ B i,

have h1 : ∀ i, x ∈ A i ∩ B i,

from mem_Inter.mp h,

have h2 : ∀ i, x ∈ A i,

from assume i, and.left (h1 i),

have h3 : ∀ i, x ∈ B i,

from assume i, and.right (h1 i),

have h4 : x ∈ ⋂ i, A i,

from mem_Inter.mpr h2,

have h5 : x ∈ ⋂ i, B i,

from mem_Inter.mpr h3,

show x ∈ (⋂ i, A i) ∩ (⋂ i, B i),

from and.intro h4 h5)

( assume h : x ∈ (⋂ i, A i) ∩ (⋂ i, B i),

have h1 : ∀ i, x ∈ A i,

from mem_Inter.mp (and.left h),

have h2 : ∀ i, x ∈ B i,

from mem_Inter.mp (and.right h),

have h3 : ∀ i, x ∈ A i ∩ B i,

from assume i, and.intro (h1 i) (h2 i),

show x ∈ ⋂ i, A i ∩ B i,

from mem_Inter.mpr h3)

-- 3ª demostración

example :

(⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=

-- by library_search

Inter_inter_distrib A B

-- 4ª demostración

example :

(⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=

ext (by finish)

ForMatUS: Pertenencia a uniones e intersecciones de familias en Lean

PorJosé A. Alonso 29 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de la caracterización de la pertenencia a uniones o intersecciones de familias de conjuntos.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.set

open set

variables {I U : Type}
variables {A : I → set U}
variable  {x : U}

-- ----------------------------------------------------
-- Ej. 1. Demostrar que
--    (x ∈ ⋃ i, A i) ↔ (∃ i, x ∈ A i)
-- ----------------------------------------------------

-- 1ª demostración
example :
  (x ∈ ⋃ i, A i) ↔ (∃ i, x ∈ A i) :=
-- by library_search
mem_Union

-- 2ª demostración
example :
  (x ∈ ⋃ i, A i) ↔ (∃ i, x ∈ A i) :=
by simp

-- ----------------------------------------------------
-- Ej. 2. Demostrar que
--    (x ∈ ⋂ i, A i) ↔ (∀ i, x ∈ A i)
-- ----------------------------------------------------

-- 1ª demostración
example :
  (x ∈ ⋂ i, A i) ↔ (∀ i, x ∈ A i) :=
-- by library_search
mem_Inter

-- 2ª demostración
example :
  (x ∈ ⋂ i, A i) ↔ (∀ i, x ∈ A i) :=
by simp

import data.set

open set

variables {I U : Type}

variables {A : I → set U}

variable {x : U}

-- ----------------------------------------------------

-- Ej. 1. Demostrar que

-- (x ∈ ⋃ i, A i) ↔ (∃ i, x ∈ A i)

-- ----------------------------------------------------

-- 1ª demostración

example :

(x ∈ ⋃ i, A i) ↔ (∃ i, x ∈ A i) :=

-- by library_search

mem_Union

-- 2ª demostración

example :

(x ∈ ⋃ i, A i) ↔ (∃ i, x ∈ A i) :=

by simp

-- ----------------------------------------------------

-- Ej. 2. Demostrar que

-- (x ∈ ⋂ i, A i) ↔ (∀ i, x ∈ A i)

-- ----------------------------------------------------

-- 1ª demostración

example :

(x ∈ ⋂ i, A i) ↔ (∀ i, x ∈ A i) :=

-- by library_search

mem_Inter

-- 2ª demostración

example :

(x ∈ ⋂ i, A i) ↔ (∀ i, x ∈ A i) :=

by simp

ForMatUS: Unión e intersección de familias de conjuntos en Lean

PorJosé A. Alonso 29 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan cómo definir en Lean la unión e intersección de familias de conjuntos y caracterizar la relación de pertenencia.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Ej. 1. Declarar I y U como variables de tipo.
-- ----------------------------------------------------

variables {I U : Type}

-- ----------------------------------------------------
-- Ej. 2. Definir la función
--    Union : (I → set U) → set U
-- tal que (Union A) es la unión de de los conjuntos de
-- la familia A.
-- ----------------------------------------------------

def Union (A : I → set U) : set U :=
  { x | ∃ i : I, x ∈ A i }

-- ----------------------------------------------------
-- Ej. 3. Definir la función
--    Inter : (I → set U) → set U
-- tal que (Inter A) es la intersección de de los
-- conjuntos de la familia A.
-- ----------------------------------------------------

def Inter (A : I → set U) : set U :=
  { x | ∀ i : I, x ∈ A i }

-- ----------------------------------------------------
-- Ej. 4. Declarar
-- + x como una variable sobre U y
-- + A como una variable sobre familas de conjuntos de
--   U con índice en A.
-- ----------------------------------------------------

variable x : U
variable (A : I → set U)

-- ----------------------------------------------------
-- Ej. 5. Demostrar que
--    x ∈ Union A ⊢ ∃ i, x ∈ A i
-- ----------------------------------------------------

example
  (h : x ∈ Union A)
  : ∃ i, x ∈ A i :=
h

-- ----------------------------------------------------
-- Ej. 6. Demostrar que
--    x ∈ x ∈ Inter A ⊢ ∀ i, x ∈ A i
-- ----------------------------------------------------

example
  (h : x ∈ Inter A)
  : ∀ i, x ∈ A i :=
h

-- ----------------------------------------------------
-- Ej 7. Usar (⋃ i, A i) como notación para (Union A).
-- ----------------------------------------------------

notation `⋃` binders `, ` r:(scoped f, Union f) := r

-- ----------------------------------------------------
-- Ej 8. Usar (⋂ i, A i) como notación para (Inter A).
-- ----------------------------------------------------

notation `⋂` binders `, ` r:(scoped f, Inter f) := r


-- ----------------------------------------------------
-- Ej. 9. Demostrar que
--    x ∈ ⋃ i, A i ⊢ ∃ i, x ∈ A i
-- ----------------------------------------------------

example
  (h : x ∈ ⋃ i, A i)
  : ∃ i, x ∈ A i :=
h

-- ----------------------------------------------------
-- Ej. 10. Demostrar que
--    x ∈ x ∈ ⋂ i, A i ⊢ ∀ i, x ∈ A i
-- ----------------------------------------------------

example
  (h : x ∈ ⋂ i, A i)
  : ∀ i, x ∈ A i :=
h

-- ----------------------------------------------------

-- Ej. 1. Declarar I y U como variables de tipo.

-- ----------------------------------------------------

variables {I U : Type}

-- ----------------------------------------------------

-- Ej. 2. Definir la función

-- Union : (I → set U) → set U

-- tal que (Union A) es la unión de de los conjuntos de

-- la familia A.

-- ----------------------------------------------------

def Union (A : I → set U) : set U :=

{ x | ∃ i : I, x ∈ A i }

-- ----------------------------------------------------

-- Ej. 3. Definir la función

-- Inter : (I → set U) → set U

-- tal que (Inter A) es la intersección de de los

-- conjuntos de la familia A.

-- ----------------------------------------------------

def Inter (A : I → set U) : set U :=

{ x | ∀ i : I, x ∈ A i }

-- ----------------------------------------------------

-- Ej. 4. Declarar

-- + x como una variable sobre U y

-- + A como una variable sobre familas de conjuntos de

-- U con índice en A.

-- ----------------------------------------------------

variable x : U

variable (A : I → set U)

-- ----------------------------------------------------

-- Ej. 5. Demostrar que

-- x ∈ Union A ⊢ ∃ i, x ∈ A i

-- ----------------------------------------------------

example

(h : x ∈ Union A)

: ∃ i, x ∈ A i :=

-- ----------------------------------------------------

-- Ej. 6. Demostrar que

-- x ∈ x ∈ Inter A ⊢ ∀ i, x ∈ A i

-- ----------------------------------------------------

example

(h : x ∈ Inter A)

: ∀ i, x ∈ A i :=

-- ----------------------------------------------------

-- Ej 7. Usar (⋃ i, A i) como notación para (Union A).

-- ----------------------------------------------------

notation `⋃` binders `, ` r:(scoped f, Union f) := r

-- ----------------------------------------------------

-- Ej 8. Usar (⋂ i, A i) como notación para (Inter A).

-- ----------------------------------------------------

notation `⋂` binders `, ` r:(scoped f, Inter f) := r

-- ----------------------------------------------------

-- Ej. 9. Demostrar que

-- x ∈ ⋃ i, A i ⊢ ∃ i, x ∈ A i

-- ----------------------------------------------------

example

(h : x ∈ ⋃ i, A i)

: ∃ i, x ∈ A i :=

-- ----------------------------------------------------

-- Ej. 10. Demostrar que

-- x ∈ x ∈ ⋂ i, A i ⊢ ∀ i, x ∈ A i

-- ----------------------------------------------------

example

(h : x ∈ ⋂ i, A i)

: ∀ i, x ∈ A i :=