(P → Q) ↔ ¬P ∨ Q
Demostrar con Lean4 que
\[ (P → Q) ↔ ¬P ∨ Q \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable (P Q : Prop) example : (P → Q) ↔ ¬P ∨ Q := by sorry |
Demostrar con Lean4 que
\[ (P → Q) ↔ ¬P ∨ Q \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable (P Q : Prop) example : (P → Q) ↔ ¬P ∨ Q := by sorry |