DAO: La semana en Calculemus (del 18 al 23 de abril)

Esta semana he publicado en Calculemus las soluciones de los siguientes problemas:

1. Propiedad de monotonía de la intersección
2. Propiedad distributiva de la intersección sobre la unión
3. Diferencia de diferencia de conjuntos

A continuación se muestran las soluciones.

1. 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

import data.set.basic

open set

variable {α : Type}

variables s t u : set α

example

(h : s ⊆ t)

: s ∩ u ⊆ t ∩ u :=

sorry

Soluciones con Lean

import data.set.basic
import tactic

open set

variable {α : Type}
variables s t u : set α

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

example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
begin
  rw subset_def,
  rw inter_def,
  rw inter_def,
  dsimp,
  intros x h1,
  cases h1 with xs xu,
  split,
  { rw subset_def at h,
    apply h,
    exact xs, },
  { exact xu, },
end

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

example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
begin
  rw [subset_def, inter_def, inter_def],
  dsimp,
  rintros x ⟨xs, xu⟩,
  rw subset_def at h,
  exact ⟨h x xs, xu⟩,
end

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

example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
begin
  simp only [subset_def, inter_def, inter_def],
  rintros x ⟨xs, xu⟩,
  rw subset_def at h,
  exact ⟨h _ xs, xu⟩,
end

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

example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
begin
  intros x xsu,
  exact ⟨h xsu.1, xsu.2⟩,
end

-- 5ª demostración
-- ===============

example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
begin
  rintros x ⟨xs, xu⟩,
  exact ⟨h xs, xu⟩,
end

-- 6ª demostración
-- ===============

example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
-- by library_search
inter_subset_inter_left u h

-- 7ª demostración
-- ===============

example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
by tidy

import data.set.basic

import tactic

open set

variable {α : Type}

variables s t u : set α

-- 1ª demostración

-- ===============

example

(h : s ⊆ t)

: s ∩ u ⊆ t ∩ u :=

begin

rw subset_def,

rw inter_def,

dsimp,

intros x h1,

cases h1 with xs xu,

split,

{ rw subset_def at h,

apply h,

exact xs, },

{ exact xu, },

end

-- 2ª demostración

-- ===============

example

(h : s ⊆ t)

: s ∩ u ⊆ t ∩ u :=

begin

rw [subset_def, inter_def, inter_def],

dsimp,

rintros x ⟨xs, xu⟩,

rw subset_def at h,

exact ⟨h x xs, xu⟩,

end

-- 3ª demostración

-- ===============

example

(h : s ⊆ t)

: s ∩ u ⊆ t ∩ u :=

begin

simp only [subset_def, inter_def, inter_def],

rintros x ⟨xs, xu⟩,

rw subset_def at h,

exact ⟨h _ xs, xu⟩,

end

-- 4ª demostración

-- ===============

example

(h : s ⊆ t)

: s ∩ u ⊆ t ∩ u :=

begin

intros x xsu,

exact ⟨h xsu.1, xsu.2⟩,

end

-- 5ª demostración

-- ===============

example

(h : s ⊆ t)

: s ∩ u ⊆ t ∩ u :=

begin

rintros x ⟨xs, xu⟩,

exact ⟨h xs, xu⟩,

end

-- 6ª demostración

-- ===============

example

(h : s ⊆ t)

: s ∩ u ⊆ t ∩ u :=

-- by library_search

inter_subset_inter_left u h

-- 7ª demostración

-- ===============

example

(h : s ⊆ t)

: s ∩ u ⊆ t ∩ u :=

by tidy

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

La construcción de las demostraciones se muestra en el siguiente vídeo

Soluciones con Isabelle/HOL

theory Propiedad_de_monotonia_de_la_interseccion
imports Main
begin

(* 1ª solución *)
lemma
  assumes "s ⊆ t"
  shows   "s ∩ u ⊆ t ∩ u"
proof  (rule subsetI)
  fix x
  assume hx: "x ∈ s ∩ u"
  have xs: "x ∈ s"
    using hx
    by (simp only: IntD1)
  then have xt: "x ∈ t"
    using assms
    by (simp only: subset_eq)
  have xu: "x ∈ u"
    using hx
    by (simp only: IntD2)
  show "x ∈ t ∩ u"
    using xt xu
    by (simp only: Int_iff)
qed

(* 2 solución *)
lemma
  assumes "s ⊆ t"
  shows   "s ∩ u ⊆ t ∩ u"
proof
  fix x
  assume hx: "x ∈ s ∩ u"
  have xs: "x ∈ s"
    using hx
    by simp
  then have xt: "x ∈ t"
    using assms
    by auto
  have xu: "x ∈ u"
    using hx
    by simp
  show "x ∈ t ∩ u"
    using xt xu
    by simp
qed

(* 3ª solución *)
lemma
  assumes "s ⊆ t"
  shows   "s ∩ u ⊆ t ∩ u"
using assms
by auto

(* 4ª solución *)
lemma
  "s ⊆ t ⟹ s ∩ u ⊆ t ∩ u"
by auto

end

theory Propiedad_de_monotonia_de_la_interseccion

imports Main

begin

(* 1ª solución *)

lemma

assumes "s ⊆ t"

shows "s ∩ u ⊆ t ∩ u"

proof (rule subsetI)

fix x

assume hx: "x ∈ s ∩ u"

have xs: "x ∈ s"

using hx

by (simp only: IntD1)

then have xt: "x ∈ t"

using assms

by (simp only: subset_eq)

have xu: "x ∈ u"

using hx

by (simp only: IntD2)

show "x ∈ t ∩ u"

using xt xu

by (simp only: Int_iff)

qed

(* 2 solución *)

lemma

assumes "s ⊆ t"

shows "s ∩ u ⊆ t ∩ u"

proof

fix x

assume hx: "x ∈ s ∩ u"

have xs: "x ∈ s"

using hx

by simp

then have xt: "x ∈ t"

using assms

by auto

have xu: "x ∈ u"

using hx

by simp

show "x ∈ t ∩ u"

using xt xu

by simp

qed

(* 3ª solución *)

lemma

assumes "s ⊆ t"

shows "s ∩ u ⊆ t ∩ u"

using assms

by auto

(* 4ª solución *)

lemma

"s ⊆ t ⟹ s ∩ u ⊆ t ∩ u"

by auto

end

2. Propiedad distributiva 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

import data.set.basic

open set

variable {α : Type}

variables s t u : set α

example :

s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=

sorry

Soluciones con Lean

import data.set.basic
import tactic

open set

variable {α : Type}
variables s t u : set α

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

example :
  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
begin
  intros x hx,
  cases hx with hxs hxtu,
  cases hxtu with hxt hxu,
  { left,
    split,
    { exact hxs, },
    { exact hxt, }},
  { right,
    split,
    { exact hxs, },
    { exact hxu, }},
end

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

example :
  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
begin
  rintros x ⟨hxs, hxt | hxu⟩,
  { left,
    exact ⟨hxs, hxt⟩, },
  { right,
    exact ⟨hxs, hxu⟩, },
end

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

example :
  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
begin
  rintros x ⟨hxs, hxt | hxu⟩,
  { exact or.inl ⟨hxs, hxt⟩, },
  { exact or.inr ⟨hxs, hxu⟩, },
end

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

example :
  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
begin
  intros x hx,
  by finish,
end

-- 5ª demostración
-- ===============

example :
  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
by rw inter_union_distrib_left

import data.set.basic

import tactic

open set

variable {α : Type}

variables s t u : set α

-- 1ª demostración

-- ===============

example :

s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=

begin

intros x hx,

cases hx with hxs hxtu,

cases hxtu with hxt hxu,

{ left,

split,

{ exact hxs, },

{ exact hxt, }},

{ right,

split,

{ exact hxs, },

{ exact hxu, }},

end

-- 2ª demostración

-- ===============

example :

s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=

begin

rintros x ⟨hxs, hxt | hxu⟩,

{ left,

exact ⟨hxs, hxt⟩, },

{ right,

exact ⟨hxs, hxu⟩, },

end

-- 3ª demostración

-- ===============

example :

s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=

begin

rintros x ⟨hxs, hxt | hxu⟩,

{ exact or.inl ⟨hxs, hxt⟩, },

{ exact or.inr ⟨hxs, hxu⟩, },

end

-- 4ª demostración

-- ===============

example :

s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=

begin

intros x hx,

by finish,

end

-- 5ª demostración

-- ===============

example :

s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=

by rw inter_union_distrib_left

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

La construcción de las demostraciones se muestra en el siguiente vídeo

Soluciones con Isabelle/HOL

theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union
imports Main
begin

(* 1ª demostración *)
lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"
proof (rule subsetI)
  fix x
  assume hx : "x ∈ s ∩ (t ∪ u)"
  then have xs : "x ∈ s"
    by (simp only: IntD1)
  have xtu: "x ∈ t ∪ u"
    using hx by (simp only: IntD2)
  then have "x ∈ t ∨ x ∈ u"
    by (simp only: Un_iff)
  then show " x ∈ s ∩ t ∪ s ∩ u"
  proof (rule disjE)
    assume xt : "x ∈ t"
    have xst : "x ∈ s ∩ t"
      using xs xt by (simp only: Int_iff)
    then show "x ∈ (s ∩ t) ∪ (s ∩ u)"
      by (simp only: UnI1)
  next
    assume xu : "x ∈ u"
    have xst : "x ∈ s ∩ u"
      using xs xu by (simp only: Int_iff)
    then show "x ∈ (s ∩ t) ∪ (s ∩ u)"
      by (simp only: UnI2)
  qed
qed

(* 2ª demostración *)
lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"
proof
  fix x
  assume hx : "x ∈ s ∩ (t ∪ u)"
  then have xs : "x ∈ s"
    by simp
  have xtu: "x ∈ t ∪ u"
    using hx by simp
  then have "x ∈ t ∨ x ∈ u"
    by simp
  then show " x ∈ s ∩ t ∪ s ∩ u"
  proof
    assume xt : "x ∈ t"
    have xst : "x ∈ s ∩ t"
      using xs xt by simp
    then show "x ∈ (s ∩ t) ∪ (s ∩ u)"
      by simp
  next
    assume xu : "x ∈ u"
    have xst : "x ∈ s ∩ u"
      using xs xu by simp
    then show "x ∈ (s ∩ t) ∪ (s ∩ u)"
      by simp
  qed
qed

(* 3ª demostración *)
lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"
proof (rule subsetI)
  fix x
  assume hx : "x ∈ s ∩ (t ∪ u)"
  then have xs : "x ∈ s"
    by (simp only: IntD1)
  have xtu: "x ∈ t ∪ u"
    using hx by (simp only: IntD2)
  then show " x ∈ s ∩ t ∪ s ∩ u"
  proof (rule UnE)
    assume xt : "x ∈ t"
    have xst : "x ∈ s ∩ t"
      using xs xt by (simp only: Int_iff)
    then show "x ∈ (s ∩ t) ∪ (s ∩ u)"
      by (simp only: UnI1)
  next
    assume xu : "x ∈ u"
    have xst : "x ∈ s ∩ u"
      using xs xu by (simp only: Int_iff)
    then show "x ∈ (s ∩ t) ∪ (s ∩ u)"
      by (simp only: UnI2)
  qed
qed

(* 4ª demostración *)
lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"
proof
  fix x
  assume hx : "x ∈ s ∩ (t ∪ u)"
  then have xs : "x ∈ s"
    by simp
  have xtu: "x ∈ t ∪ u"
    using hx by simp
  then show " x ∈ s ∩ t ∪ s ∩ u"
  proof (rule UnE)
    assume xt : "x ∈ t"
    have xst : "x ∈ s ∩ t"
      using xs xt by simp
    then show "x ∈ (s ∩ t) ∪ (s ∩ u)"
      by simp
  next
    assume xu : "x ∈ u"
    have xst : "x ∈ s ∩ u"
      using xs xu by simp
    then show "x ∈ (s ∩ t) ∪ (s ∩ u)"
      by simp
  qed
qed

(* 5ª demostración *)
lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"
by (simp only: Int_Un_distrib)

(* 6ª demostración *)
lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"
by auto

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union

imports Main

begin

(* 1ª demostración *)

lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"

proof (rule subsetI)

fix x

assume hx : "x ∈ s ∩ (t ∪ u)"

then have xs : "x ∈ s"

by (simp only: IntD1)

have xtu: "x ∈ t ∪ u"

using hx by (simp only: IntD2)

then have "x ∈ t ∨ x ∈ u"

by (simp only: Un_iff)

then show " x ∈ s ∩ t ∪ s ∩ u"

proof (rule disjE)

assume xt : "x ∈ t"

have xst : "x ∈ s ∩ t"

using xs xt by (simp only: Int_iff)

then show "x ∈ (s ∩ t) ∪ (s ∩ u)"

by (simp only: UnI1)

assume xu : "x ∈ u"

have xst : "x ∈ s ∩ u"

using xs xu by (simp only: Int_iff)

then show "x ∈ (s ∩ t) ∪ (s ∩ u)"

by (simp only: UnI2)

qed

(* 2ª demostración *)

lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"

proof

fix x

assume hx : "x ∈ s ∩ (t ∪ u)"

then have xs : "x ∈ s"

by simp

have xtu: "x ∈ t ∪ u"

using hx by simp

then have "x ∈ t ∨ x ∈ u"

by simp

then show " x ∈ s ∩ t ∪ s ∩ u"

proof

assume xt : "x ∈ t"

have xst : "x ∈ s ∩ t"

using xs xt by simp

then show "x ∈ (s ∩ t) ∪ (s ∩ u)"

by simp

assume xu : "x ∈ u"

have xst : "x ∈ s ∩ u"

using xs xu by simp

then show "x ∈ (s ∩ t) ∪ (s ∩ u)"

by simp

qed

(* 3ª demostración *)

lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"

proof (rule subsetI)

fix x

assume hx : "x ∈ s ∩ (t ∪ u)"

then have xs : "x ∈ s"

by (simp only: IntD1)

have xtu: "x ∈ t ∪ u"

using hx by (simp only: IntD2)

then show " x ∈ s ∩ t ∪ s ∩ u"

proof (rule UnE)

assume xt : "x ∈ t"

have xst : "x ∈ s ∩ t"

using xs xt by (simp only: Int_iff)

then show "x ∈ (s ∩ t) ∪ (s ∩ u)"

by (simp only: UnI1)

assume xu : "x ∈ u"

have xst : "x ∈ s ∩ u"

using xs xu by (simp only: Int_iff)

then show "x ∈ (s ∩ t) ∪ (s ∩ u)"

by (simp only: UnI2)

qed

(* 4ª demostración *)

lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"

proof

fix x

assume hx : "x ∈ s ∩ (t ∪ u)"

then have xs : "x ∈ s"

by simp

have xtu: "x ∈ t ∪ u"

using hx by simp

then show " x ∈ s ∩ t ∪ s ∩ u"

proof (rule UnE)

assume xt : "x ∈ t"

have xst : "x ∈ s ∩ t"

using xs xt by simp

then show "x ∈ (s ∩ t) ∪ (s ∩ u)"

by simp

assume xu : "x ∈ u"

have xst : "x ∈ s ∩ u"

using xs xu by simp

then show "x ∈ (s ∩ t) ∪ (s ∩ u)"

by simp

qed

(* 5ª demostración *)

lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"

by (simp only: Int_Un_distrib)

(* 6ª demostración *)

lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"

by auto

end

3. 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

import data.set.basic

open set

variable {α : Type}

variables s t u : set α

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=

sorry

Soluciones con Lean

import data.set.basic
open set

variable {α : Type}
variables s t u : set α

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

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=
begin
  intros x hx,
  cases hx with hxst hxnu,
  cases hxst with hxs hxnt,
  split,
  { exact hxs },
  { dsimp,
    by_contradiction hxtu,
    cases hxtu with hxt hxu,
    { apply hxnt,
      exact hxt, },
    { apply hxnu,
      exact hxu, }},
end

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

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=
begin
  rintros x ⟨⟨hxs, hxnt⟩, hxnu⟩,
  split,
  { exact hxs },
  { by_contradiction hxtu,
    cases hxtu with hxt hxu,
    { exact hxnt hxt, },
    { exact hxnu hxu, }},
end

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

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=
begin
  rintros x ⟨⟨xs, xnt⟩, xnu⟩,
  use xs,
  rintros (xt | xu),
  { contradiction, },
  { contradiction, },
end

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

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=
begin
  rintros x ⟨⟨xs, xnt⟩, xnu⟩,
  use xs,
  rintros (xt | xu); contradiction,
end

-- 5ª demostración
-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=
begin
  intros x xstu,
  simp at *,
  finish,
end

-- 6ª demostración
-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=
begin
  intros x xstu,
  finish,
end

-- 7ª demostración
-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=
by rw diff_diff

-- 8ª demostración
-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=
by tidy

import data.set.basic

open set

variable {α : Type}

variables s t u : set α

-- 1ª demostración

-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=

begin

intros x hx,

cases hx with hxst hxnu,

cases hxst with hxs hxnt,

split,

{ exact hxs },

{ dsimp,

by_contradiction hxtu,

cases hxtu with hxt hxu,

{ apply hxnt,

exact hxt, },

{ apply hxnu,

exact hxu, }},

end

-- 2ª demostración

-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=

begin

rintros x ⟨⟨hxs, hxnt⟩, hxnu⟩,

split,

{ exact hxs },

{ by_contradiction hxtu,

cases hxtu with hxt hxu,

{ exact hxnt hxt, },

{ exact hxnu hxu, }},

end

-- 3ª demostración

-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=

begin

rintros x ⟨⟨xs, xnt⟩, xnu⟩,

use xs,

rintros (xt | xu),

{ contradiction, },

end

-- 4ª demostración

-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=

begin

rintros x ⟨⟨xs, xnt⟩, xnu⟩,

use xs,

rintros (xt | xu); contradiction,

end

-- 5ª demostración

-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=

begin

intros x xstu,

simp at *,

finish,

end

-- 6ª demostración

-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=

begin

intros x xstu,

finish,

end

-- 7ª demostración

-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=

by rw diff_diff

-- 8ª demostración

-- ===============

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=

by tidy

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

La construcción de las demostraciones se muestra en el siguiente vídeo

Soluciones con Isabelle/HOL

theory Diferencia_de_diferencia_de_conjuntos
imports Main
begin

(* 1ª demostración *)
lemma "(s - t) - u ⊆ s - (t ∪ u)"
proof (rule subsetI)
  fix x
  assume hx : "x ∈ (s - t) - u"
  then show "x ∈ s - (t ∪ u)"
  proof (rule DiffE)
    assume xst : "x ∈ s - t"
    assume xnu : "x ∉ u"
    note xst
    then show "x ∈ s - (t ∪ u)"
    proof (rule DiffE)
      assume xs : "x ∈ s"
      assume xnt : "x ∉ t"
      have xntu : "x ∉ t ∪ u"
      proof (rule notI)
        assume xtu : "x ∈ t ∪ u"
        then show False
        proof (rule UnE)
          assume xt : "x ∈ t"
          with xnt show False
            by (rule notE)
        next
          assume xu : "x ∈ u"
          with xnu show False
            by (rule notE)
        qed
      qed
      show "x ∈ s - (t ∪ u)"
        using xs xntu by (rule DiffI)
    qed
  qed
qed

(* 2ª demostración *)
lemma "(s - t) - u ⊆ s - (t ∪ u)"
proof
  fix x
  assume hx : "x ∈ (s - t) - u"
  then have xst : "x ∈ (s - t)"
    by simp
  then have xs : "x ∈ s"
    by simp
  have xnt : "x ∉ t"
    using xst by simp
  have xnu : "x ∉ u"
    using hx by simp
  have xntu : "x ∉ t ∪ u"
    using xnt xnu by simp
  then show "x ∈ s - (t ∪ u)"
    using xs by simp
qed

(* 3ª demostración *)
lemma "(s - t) - u ⊆ s - (t ∪ u)"
proof
  fix x
  assume "x ∈ (s - t) - u"
  then show "x ∈ s - (t ∪ u)"
     by simp
qed

(* 4ª demostración *)
lemma "(s - t) - u ⊆ s - (t ∪ u)"
by auto

theory Diferencia_de_diferencia_de_conjuntos

imports Main

begin

(* 1ª demostración *)

lemma "(s - t) - u ⊆ s - (t ∪ u)"

proof (rule subsetI)

fix x

assume hx : "x ∈ (s - t) - u"

then show "x ∈ s - (t ∪ u)"

proof (rule DiffE)

assume xst : "x ∈ s - t"

assume xnu : "x ∉ u"

note xst

then show "x ∈ s - (t ∪ u)"

proof (rule DiffE)

assume xs : "x ∈ s"

assume xnt : "x ∉ t"

have xntu : "x ∉ t ∪ u"

proof (rule notI)

assume xtu : "x ∈ t ∪ u"

then show False

proof (rule UnE)

assume xt : "x ∈ t"

with xnt show False

by (rule notE)

assume xu : "x ∈ u"

with xnu show False

by (rule notE)

qed

show "x ∈ s - (t ∪ u)"

using xs xntu by (rule DiffI)

qed

(* 2ª demostración *)

lemma "(s - t) - u ⊆ s - (t ∪ u)"

proof

fix x

assume hx : "x ∈ (s - t) - u"

then have xst : "x ∈ (s - t)"

by simp

then have xs : "x ∈ s"

by simp

have xnt : "x ∉ t"

using xst by simp

have xnu : "x ∉ u"

using hx by simp

have xntu : "x ∉ t ∪ u"

using xnt xnu by simp

then show "x ∈ s - (t ∪ u)"

using xs by simp

qed

(* 3ª demostración *)

lemma "(s - t) - u ⊆ s - (t ∪ u)"

proof

fix x

assume "x ∈ (s - t) - u"

then show "x ∈ s - (t ∪ u)"

by simp

qed

(* 4ª demostración *)

lemma "(s - t) - u ⊆ s - (t ∪ u)"

by auto

1. Propiedad de monotonía de la intersección

2. Propiedad distributiva de la intersección sobre la unión

3. Diferencia de diferencia de conjuntos

Se puede imprimir o compartir con