Unión con su intersección

Demostrar que

s ∪ (s ∩ t) = s

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

import data.set.basic
open set

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

example : s ∪ (s ∩ t) = s :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t : set α

example : s ∪ (s ∩ t) = s :=

sorry

Soluciones con Lean

import data.set.basic
open set

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

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

example : s ∪ (s ∩ t) = s :=
begin
  ext x,
  split,
  { intro hx,
    cases hx with xs xst,
    { exact xs, },
    { exact xst.1, }},
  { intro xs,
    left,
    exact xs, },
end

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

example : s ∪ (s ∩ t) = s :=
begin
  ext x,
  exact ⟨λ hx, or.dcases_on hx id and.left,
         λ xs, or.inl xs⟩,
end

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

example : s ∪ (s ∩ t) = s :=
begin
  ext x,
  split,
  { rintros (xs | ⟨xs, xt⟩);
    exact xs },
  { intro xs,
    left,
    exact xs },
end

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

example : s ∪ (s ∩ t) = s :=
sup_inf_self

import data.set.basic

open set

variable {α : Type}

variables s t : set α

-- 1ª demostración

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

example : s ∪ (s ∩ t) = s :=

begin

ext x,

split,

{ intro hx,

cases hx with xs xst,

{ exact xs, },

{ exact xst.1, }},

{ intro xs,

left,

exact xs, },

end

-- 2ª demostración

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

example : s ∪ (s ∩ t) = s :=

begin

ext x,

exact ⟨λ hx, or.dcases_on hx id and.left,

λ xs, or.inl xs⟩,

end

-- 3ª demostración

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

example : s ∪ (s ∩ t) = s :=

begin

ext x,

split,

{ rintros (xs | ⟨xs, xt⟩);

exact xs },

{ intro xs,

left,

exact xs },

end

-- 4ª demostración

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

example : s ∪ (s ∩ t) = s :=

sup_inf_self

Soluciones con Isabelle/HOL

theory Union_con_su_interseccion
imports Main
begin

(* 1ª demostración *)
lemma "s ∪ (s ∩ t) = s"
proof (rule equalityI)
  show "s ∪ (s ∩ t) ⊆ s"
  proof (rule subsetI)
    fix x
    assume "x ∈ s ∪ (s ∩ t)"
    then show "x ∈ s"
    proof
      assume "x ∈ s"
      then show "x ∈ s"
        by this
    next
      assume "x ∈ s ∩ t"
      then show "x ∈ s"
        by (simp only: IntD1)
    qed
  qed
next
  show "s ⊆ s ∪ (s ∩ t)"
  proof (rule subsetI)
    fix x
    assume "x ∈ s"
    then show "x ∈ s ∪ (s ∩ t)"
      by (simp only: UnI1)
  qed
qed

(* 2ª demostración *)
lemma "s ∪ (s ∩ t) = s"
proof
  show "s ∪ s ∩ t ⊆ s"
  proof
    fix x
    assume "x ∈ s ∪ (s ∩ t)"
    then show "x ∈ s"
    proof
      assume "x ∈ s"
      then show "x ∈ s"
        by this
    next
      assume "x ∈ s ∩ t"
      then show "x ∈ s"
        by simp
    qed
  qed
next
  show "s ⊆ s ∪ (s ∩ t)"
  proof
    fix x
    assume "x ∈ s"
    then show "x ∈ s ∪ (s ∩ t)"
      by simp
  qed
qed

(* 3ª demostración *)
lemma "s ∪ (s ∩ t) = s"
  by auto

end

theory Union_con_su_interseccion

imports Main

begin

(* 1ª demostración *)

lemma "s ∪ (s ∩ t) = s"

proof (rule equalityI)

show "s ∪ (s ∩ t) ⊆ s"

proof (rule subsetI)

fix x

assume "x ∈ s ∪ (s ∩ t)"

then show "x ∈ s"

proof

assume "x ∈ s"

then show "x ∈ s"

by this

assume "x ∈ s ∩ t"

then show "x ∈ s"

by (simp only: IntD1)

qed

show "s ⊆ s ∪ (s ∩ t)"

proof (rule subsetI)

fix x

assume "x ∈ s"

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

by (simp only: UnI1)

qed

(* 2ª demostración *)

lemma "s ∪ (s ∩ t) = s"

proof

show "s ∪ s ∩ t ⊆ s"

proof

fix x

assume "x ∈ s ∪ (s ∩ t)"

then show "x ∈ s"

proof

assume "x ∈ s"

then show "x ∈ s"

by this

assume "x ∈ s ∩ t"

then show "x ∈ s"

by simp

qed

show "s ⊆ s ∪ (s ∩ t)"

proof

fix x

assume "x ∈ s"

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

by simp

qed

(* 3ª demostración *)

lemma "s ∪ (s ∩ t) = s"

by auto

end

Nuevas soluciones

En los comentarios se pueden escribir nuevas soluciones.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

Share this:

Escribe un comentarioCancel reply