Disjunction is idempotent
Closed
Theorem & proof
·
or_self_idem.lean
·
✓ verified
1
2
3
4
import Mathlib theorem or_self_idem (p : Prop) : (p ∨ p) ↔ p := Iff.intro (fun h => h.elim id id) Or.inl
Rewards pledged
No rewards pledged yet.