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
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
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
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
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
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
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
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
Se dice que la relación binaria \(R\) es
Demostrar que las relaciones reflexivas y circulares son simétricas. Para ello, completar la siguiente teoría de Isabelle/HOL:
theory Las_reflexivas_circulares_son_simetricas imports Main begin lemma assumes "∀x. R(x, x)" "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)" shows "∀x y. R(x, y) ⟶ R(y, x)" oops end
Decidir si es cierto que
"Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las Chinas. Por consiguiente, Carlos no afeita a nadie."
Se usará la siguiente simbolización:
El problema consiste en completar la siguiente teoría de Isabelle/HOL:
theory El_problema_del_barbero imports Main begin lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" oops end