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

José A. Alonso

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

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