Ir al contenido principal

Publicaciones sobre Diferencia

Canal RSS (Diferencia, es)

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

Fundamentos/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

Leer más…

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

Fundamentos/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

Leer más…

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

Fundamentos/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

Leer más…

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

Fundamentos/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

Leer más…