Demostraciones de "(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)"

José A. Alonso

28-05-2021

Conjuntos

Demostrar con Lean4 y con Isabelle/HOL que \[ (s \setminus t) ∪ (t \setminus s) = (s ∪ t) \setminus (s ∩ t) \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α : Type}
variable (s t : Set α)

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

y la siguiente teoría de Isabelle/HOL:

theory Diferencia_de_union_e_interseccion
imports Main
begin

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

end

Demostraciones de "(s \ t) ∪ t = s ∪ t"

José A. Alonso

27-05-2021

Conjuntos

Demostrar con Lean4 y con Isabelle/HOL que \[ (s \setminus t) ∪ t = s ∪ t \]

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

import Mathlib.Data.Set.Basic
open Set

variable {α : Type}
variable (s t : Set α)

example : (s \\setminus t) ∪ t = s ∪ t :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Union_con_su_diferencia
imports Main
begin

lemma "(s - t) ∪ t = s ∪ t"
oops

end

Demostraciones de "s ∪ (s ∩ t) = s"

José A. Alonso

26-05-2021

Conjuntos

Demostrar con Lean4 y con Isabelle/HOL que \[ s ∪ (s ∩ t) = s \]

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

import Mathlib.Data.Set.Basic
open Set
variable {α : Type}
variable (s t : Set α)

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

y la siguiente teoría de Isabelle/HOL:

theory Union_con_su_interseccion
imports Main
begin

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

end

Demostraciones de "s ∩ (s ∪ t) = s"

José A. Alonso

25-05-2021

Conjuntos

Demostrar con Lean4 y con Isabelle/HOL que \[ s ∩ (s ∪ t) = s \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s t : Set α)

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

y la siguiente teoría de Isabelle/HOL:

theory Interseccion_con_su_union
imports Main
begin

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

wnd

Demostraciones de "s ∩ t = t ∩ s"

José A. Alonso

24-05-2021

Conjuntos

Demostrar con Lean4 y con Isabelle/HOL que \[ s ∩ t = t ∩ s \]

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

import Mathlib.Data.Set.Basic
open Set
variable {α : Type}
variable (s t : Set α)

example : s ∩ t = t ∩ s :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Conmutatividad_de_la_interseccion
imports Main
begin

lemma "s ∩ t = t ∩ s"
oops

end

Demostraciones de "s \ (t ∪ u) ⊆ (s \ t) \ u"

José A. Alonso

21-05-2021

Conjuntos

Demostrar con Lean4 y con Isabelle/HOL que \[ s \setminus (t ∪ u) ⊆ (s \setminus t) \setminus u \]

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

import Mathlib.Data.Set.Basic
open Set
variable {α : Type}
variable (s t u : Set α)

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

y la siguiente teoría de Isabelle/HOL:

theory Diferencia_de_diferencia_de_conjuntos_2
imports Main
begin

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

end

Demostraciones de "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)"

José A. Alonso

20-05-2021

Conjuntos

Demostrar con Lean4 y con Isabelle/HOL que \[ (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u) \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α : Type}
variable (s t u : Set α)

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

y la siguiente teoría de Isabelle/HOL:

theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union_2
imports Main
begin

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

end

Demostraciones de "(s - t) - u ⊆ s - (t ∪ u)"

José A. Alonso

19-05-2021

Conjuntos

Demostrar con Lean4 y con Isabelle/HOL que \[ (s \setminus t) \setminus u ⊆ s \setminus (t ∪ u) \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set
variable {α : Type}
variable (s t u : Set α)

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

y la la siguiente teoría de Isabelle/HOL:

theory Diferencia_de_diferencia_de_conjuntos
imports Main
begin

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

Demostraciones de "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"

José A. Alonso

18-05-2021

Conjuntos

Demostrar con Lean4 y con Isabelle/HOL que \[s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)\]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s t u : Set α)

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

y la siguiente teoría de Isabelle/HOL:

theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union
imports Main
begin

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

end

Demostraciones de "Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u"

José A. Alonso

17-05-2021

Conjuntos

Demostrar con Lean4 e Isabelle/HOL que

Si \(s ⊆ t\), entonces \(s ∩ u ⊆ t ∩ u\).

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s t u : Set α)

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

y la siguiente teoría de Isabelle/HOL:

theory Propiedad_de_monotonia_de_la_interseccion
imports Main
begin

lemma
  assumes "s ⊆ t"
  shows   "s ∩ u ⊆ t ∩ u"
oops

end