La paradoja del barbero
Demostrar con Lean4 la paradoja del barbero; es decir, que no existe un hombre que afeite a todos los que no se afeitan a sí mismo y sólo a los que no se afeitan a sí mismo.
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable (Hombre : Type) variable (afeita : Hombre → Hombre → Prop) example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := by sorry |