José A. Alonso

ForMatUS: Complementario de un conjunto en Lean (Pruebas de A \ B ⊆ Bᶜ)

PorJosé A. Alonso 26 octubre 202021 diciembre 2020

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

A \ B ⊆ Bᶜ

1	A \ B ⊆ Bᶜ

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
--    A \ B ⊆ Bᶜ
-- ----------------------------------------------------

import data.set

variable  {U : Type}
variables A B : set U
variable  x : U

open set

-- #reduce x ∈ Bᶜ
-- #reduce Bᶜ

-- 1ª demostración
example : A \ B ⊆ Bᶜ :=
begin
  intros x h,
  simp at *,
  exact h.right,
end

-- 2ª demostración
example : A \ B ⊆ Bᶜ :=
begin
  intros x h,
  exact h.right,
end

-- 3ª demostración
example : A \ B ⊆ Bᶜ :=
assume x,
assume h1 : x ∈ A \ B,
have h2 : x ∉ B, from and.right h1,
show x ∈ Bᶜ,     from h2

-- 4ª demostración
example : A \ B ⊆ Bᶜ :=
assume x,
assume h1 : x ∈ A \ B,
show x ∈ Bᶜ, from and.right h1

-- 5ª demostración
example : A \ B ⊆ Bᶜ :=
assume x,
λ h1, and.right h1

-- 6ª demostración
example : A \ B ⊆ Bᶜ :=
assume x,
and.right

-- 7ª demostración
example : A \ B ⊆ Bᶜ :=
λ _, and.right

-- 8ª demostración
example : A \ B ⊆ Bᶜ :=
λ _, not_mem_of_mem_diff

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

-- Ej. 1. Demostrar

-- A \ B ⊆ Bᶜ

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

import data.set

variable {U : Type}

variables A B : set U

variable x : U

open set

-- #reduce x ∈ Bᶜ

-- #reduce Bᶜ

-- 1ª demostración

example : A \ B ⊆ Bᶜ :=

begin

intros x h,

simp at *,

exact h.right,

end

-- 2ª demostración

example : A \ B ⊆ Bᶜ :=

begin

intros x h,

exact h.right,

end

-- 3ª demostración

example : A \ B ⊆ Bᶜ :=

assume x,

assume h1 : x ∈ A \ B,

have h2 : x ∉ B, from and.right h1,

show x ∈ Bᶜ, from h2

-- 4ª demostración

example : A \ B ⊆ Bᶜ :=

assume x,

assume h1 : x ∈ A \ B,

show x ∈ Bᶜ, from and.right h1

-- 5ª demostración

example : A \ B ⊆ Bᶜ :=

assume x,

λ h1, and.right h1

-- 6ª demostración

example : A \ B ⊆ Bᶜ :=

assume x,

and.right

-- 7ª demostración

example : A \ B ⊆ Bᶜ :=

λ _, and.right

-- 8ª demostración

example : A \ B ⊆ Bᶜ :=

λ _, not_mem_of_mem_diff

ForMatUS: Diferencia de conjuntos en Lean (Pruebas de A \ B ⊆ A)

PorJosé A. Alonso 26 octubre 202021 diciembre 2020

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

A \ B ⊆ A

A \ B ⊆ A

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
--    A \ B ⊆ A
-- ----------------------------------------------------

import data.set

variable  U : Type
variables A B : set U
variable  x : U

open set

-- #reduce (A \ B)
-- #reduce x ∈ A \ B

-- 1ª demostración
example : A \ B ⊆ A :=
begin
  intros x h,
  simp at h,
  exact h.left,
end

-- 2ª demostración
example : A \ B ⊆ A :=
begin
  intros x h,
  exact h.left,
end

-- 3ª demostración
example : A \ B ⊆ A :=
assume x,
assume h : x ∈ A \ B,
show x ∈ A, from h.left

-- 4ª demostración
example : A \ B ⊆ A :=
assume x,
assume h : x ∈ A \ B,
and.left h

-- 5ª demostración
example : A \ B ⊆ A :=
assume x,
λ h, and.left h

-- 6ª demostración
example : A \ B ⊆ A :=
assume x, and.left

-- 7ª demostración
example : A \ B ⊆ A :=
λ _, and.left

-- 8ª demostración
example : A \ B ⊆ A :=
-- by library_search
diff_subset A B

-- 9ª demostración
example : A \ B ⊆ A :=
assume x,
assume h : x ∈ A \ B,
show x ∈ A, from mem_of_mem_diff h

-- 10ª demostración
example : A \ B ⊆ A :=
λ _, mem_of_mem_diff

-- 11ª demostración
example : A \ B ⊆ A :=
by finish [subset_def]

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

-- Ej. 1. Demostrar

-- A \ B ⊆ A

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

import data.set

variable U : Type

variables A B : set U

variable x : U

open set

-- #reduce (A \ B)

-- #reduce x ∈ A \ B

-- 1ª demostración

example : A \ B ⊆ A :=

begin

intros x h,

simp at h,

exact h.left,

end

-- 2ª demostración

example : A \ B ⊆ A :=

begin

intros x h,

exact h.left,

end

-- 3ª demostración

example : A \ B ⊆ A :=

assume x,

assume h : x ∈ A \ B,

show x ∈ A, from h.left

-- 4ª demostración

example : A \ B ⊆ A :=

assume x,

assume h : x ∈ A \ B,

and.left h

-- 5ª demostración

example : A \ B ⊆ A :=

assume x,

λ h, and.left h

-- 6ª demostración

example : A \ B ⊆ A :=

assume x, and.left

-- 7ª demostración

example : A \ B ⊆ A :=

λ _, and.left

-- 8ª demostración

example : A \ B ⊆ A :=

-- by library_search

diff_subset A B

-- 9ª demostración

example : A \ B ⊆ A :=

assume x,

assume h : x ∈ A \ B,

show x ∈ A, from mem_of_mem_diff h

-- 10ª demostración

example : A \ B ⊆ A :=

λ _, mem_of_mem_diff

-- 11ª demostración

example : A \ B ⊆ A :=

by finish [subset_def]

ForMatUS: Regla del conjunto vacío en Lean

PorJosé A. Alonso 25 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 11 pruebas en Lean que ilustran la regla del conjunto vacío 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
--    ∅ ⊆ A
-- ----------------------------------------------------

import data.set

variable  U : Type
variables A : set U
variable  x : U

open set

-- #reduce (∅ : set U)
-- #reduce x ∈ (∅ : set U)

-- 1ª demostración
example : ∅ ⊆ A :=
begin
  intros x h,
  simp at h,
  exfalso,
  exact h,
end

-- 2ª demostración
example : ∅ ⊆ A :=
begin
  intros x h,
  exfalso,
  exact h,
end

-- 3ª demostración
example : ∅ ⊆ A :=
assume x,
assume h : x ∈ (∅ : set U),
show x ∈ A, from false.elim h

-- 4ª demostración
example : ∅ ⊆ A :=
λ x, λ h, false.elim h

-- 5ª demostración
example : ∅ ⊆ A :=
λ _, false.elim

-- 6ª demostración
example : ∅ ⊆ A :=
-- by library_search
empty_subset A

-- 7ª demostración
example : ∅ ⊆ A :=
assume x,
assume h : x ∈ (∅ : set U),
show x ∈ A, from absurd h (not_mem_empty x)

-- 8ª demostración
example : ∅ ⊆ A :=
λ x h, absurd h (not_mem_empty x)

-- 9ª demostración
example : ∅ ⊆ A :=
-- by hint
by tauto

-- 10ª demostración
example : ∅ ⊆ A :=
by finish

-- 11ª demostración
example : ∅ ⊆ A :=
by simp

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

-- Ej. 1. Demostrar

-- ∅ ⊆ A

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

import data.set

variable U : Type

variables A : set U

variable x : U

open set

-- #reduce (∅ : set U)

-- #reduce x ∈ (∅ : set U)

-- 1ª demostración

example : ∅ ⊆ A :=

begin

intros x h,

simp at h,

exfalso,

exact h,

end

-- 2ª demostración

example : ∅ ⊆ A :=

begin

intros x h,

exfalso,

exact h,

end

-- 3ª demostración

example : ∅ ⊆ A :=

assume x,

assume h : x ∈ (∅ : set U),

show x ∈ A, from false.elim h

-- 4ª demostración

example : ∅ ⊆ A :=

λ x, λ h, false.elim h

-- 5ª demostración

example : ∅ ⊆ A :=

λ _, false.elim

-- 6ª demostración

example : ∅ ⊆ A :=

-- by library_search

empty_subset A

-- 7ª demostración

example : ∅ ⊆ A :=

assume x,

assume h : x ∈ (∅ : set U),

show x ∈ A, from absurd h (not_mem_empty x)

-- 8ª demostración

example : ∅ ⊆ A :=

λ x h, absurd h (not_mem_empty x)

-- 9ª demostración

example : ∅ ⊆ A :=

-- by hint

by tauto

-- 10ª demostración

example : ∅ ⊆ A :=

by finish

-- 11ª demostración

example : ∅ ⊆ A :=

by simp

ForMatUS: Regla de introducción de la unión en Lean

PorJosé A. Alonso 25 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 11 pruebas en Lean de la regla de introducción de la unión 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
--    A ⊆ A ∪ B
-- ----------------------------------------------------

import data.set

variable  U : Type
variables A B : set U
variable  x : U

open set

-- #reduce x ∈ A ∪ B

-- 1ª demostración
example : A ⊆ A ∪ B :=
begin
  intros x h,
  simp,
  left,
  exact h,
end

-- 2ª demostración
example : A ⊆ A ∪ B :=
begin
  intros x h,
  left,
  exact h,
end

-- 3ª demostración
example : A ⊆ A ∪ B :=
assume x,
assume h : x ∈ A,
show x ∈ A ∪ B, from or.inl h

-- 4ª demostración
example : A ⊆ A ∪ B :=
assume x,
assume h : x ∈ A,
or.inl h

-- 5ª demostración
example : A ⊆ A ∪ B :=
assume x,
λ h : x ∈ A, or.inl h

-- 6ª demostración
example : A ⊆ A ∪ B :=
assume x, or.inl

-- 7ª demostración
example : A ⊆ A ∪ B :=
λ x, or.inl

-- 8ª demostración
example : A ⊆ A ∪ B :=
-- by library_search
subset_union_left A B

-- 9ª demostración
example : A ⊆ A ∪ B :=
λ x, mem_union_left B

-- 10ª demostración
example : A ⊆ A ∪ B :=
-- by hint
by finish

-- 11ª demostración
example : A ⊆ A ∪ B :=
by simp

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

-- Ej. 1. Demostrar

-- A ⊆ A ∪ B

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

import data.set

variable U : Type

variables A B : set U

variable x : U

open set

-- #reduce x ∈ A ∪ B

-- 1ª demostración

example : A ⊆ A ∪ B :=

begin

intros x h,

simp,

left,

exact h,

end

-- 2ª demostración

example : A ⊆ A ∪ B :=

begin

intros x h,

left,

exact h,

end

-- 3ª demostración

example : A ⊆ A ∪ B :=

assume x,

assume h : x ∈ A,

show x ∈ A ∪ B, from or.inl h

-- 4ª demostración

example : A ⊆ A ∪ B :=

assume x,

assume h : x ∈ A,

or.inl h

-- 5ª demostración

example : A ⊆ A ∪ B :=

assume x,

λ h : x ∈ A, or.inl h

-- 6ª demostración

example : A ⊆ A ∪ B :=

assume x, or.inl

-- 7ª demostración

example : A ⊆ A ∪ B :=

λ x, or.inl

-- 8ª demostración

example : A ⊆ A ∪ B :=

-- by library_search

subset_union_left A B

-- 9ª demostración

example : A ⊆ A ∪ B :=

λ x, mem_union_left B

-- 10ª demostración

example : A ⊆ A ∪ B :=

-- by hint

by finish

-- 11ª demostración

example : A ⊆ A ∪ B :=

by simp

ForMatUS: Regla de introducción de la intersección en Lean

PorJosé A. Alonso 24 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 7 pruebas en Lean de la regla de introducción de la intersección 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
--    x ∈ A → x ∈ B → x ∈ A ∩ B
-- ----------------------------------------------------

import data.set

variable  U : Type
variables A B : set U
variable  x : U

open set

-- #reduce x ∈ A ∩ B

-- 1ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
begin
  intros h1 h2,
  simp,
  split,
  { exact h1, },
  { exact h2, },
end

-- 2ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
begin
  intros h1 h2,
  split,
  { exact h1, },
  { exact h2, },
end

-- 3ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
assume h1 : x ∈ A,
assume h2 : x ∈ B,
show x ∈ A ∩ B, from and.intro h1 h2

-- 4ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
assume h1 : x ∈ A,
assume h2 : x ∈ B,
show x ∈ A ∩ B, from ⟨h1, h2⟩

-- 5ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
assume h1 : x ∈ A,
assume h2 : x ∈ B,
⟨h1, h2⟩

-- 6ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
λ h1 h2, ⟨h1, h2⟩

-- 7ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
-- by library_search
mem_inter

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

-- Ej. 1. Demostrar

-- x ∈ A → x ∈ B → x ∈ A ∩ B

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

import data.set

variable U : Type

variables A B : set U

variable x : U

open set

-- #reduce x ∈ A ∩ B

-- 1ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

begin

intros h1 h2,

simp,

split,

{ exact h1, },

{ exact h2, },

end

-- 2ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

begin

intros h1 h2,

split,

{ exact h1, },

{ exact h2, },

end

-- 3ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

assume h1 : x ∈ A,

assume h2 : x ∈ B,

show x ∈ A ∩ B, from and.intro h1 h2

-- 4ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

assume h1 : x ∈ A,

assume h2 : x ∈ B,

show x ∈ A ∩ B, from ⟨h1, h2⟩

-- 5ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

assume h1 : x ∈ A,

assume h2 : x ∈ B,

⟨h1, h2⟩

-- 6ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

λ h1 h2, ⟨h1, h2⟩

-- 7ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

-- by library_search

mem_inter