Propiedad semidistributiva 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

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

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

1. Soluciones con Lean

2. Soluciones con Isabelle/HOL

Share this:

Escribe un comentarioCancel reply