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
Decidir si es cierto que
"Existe una persona tal que si dicha persona se infecta, entonces todas las personas se infectan."
El problema consiste en completar la siguiente teoría de Isabelle/HOL:
theory El_problema_de_los_infectados imports Main begin lemma "∃x. (I x ⟶ (∀y. I y))" by sorry end
En el libro de Raymond Smullyan ¿La dama o el tigre? (en inglés, The lady or the tiger?) se plantea el siguiente problema
Un rey somete a un prisionero a la siguiente prueba: lo enfrenta a dos puertas, de las que el prisionero debe elegir una, y entrar la habitación correspondiente. Se informa al prisionero que en cada una de las habitaciones puede haber un tigre o una dama. Como es natural, el prisionero debe elegir la puerta que le lleva a la dama (entre otras cosas, para no ser devorado por el tigre). Para ayudarle, en cada puerta hay un letrero. El de la puerta 1 dice "en esta habitación hay una dama y en la otra un tigre" y el de la puerta 2 dice "en una de estas habitaciones hay una dama y en una de estas habitaciones hay un tigre"
Sabiendo que uno de los carteles dice la verdad y el otro no, demostrar que la dama se encuentra en la segunda habitación.
Para ello, completar la siguiente teoría
theory La_dama_o_el_tigre imports Main begin lemma assumes "c1 ⟷ dp ∧ ts" "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)" "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)" shows "ds" oops end
donde se han usado los siguientes símbolos