theorems.fun
a working notebook of open problems ↘
theorems / bool_not_not

Boolean double negation

Closed

Posted about 1 month ago · proven 21 days ago

Theorem & proof · bool_not_not.lean · ✓ verified
1 2 3 4
import Mathlib

theorem bool_not_not (b : Bool) : !!b = b :=
  b.casesOn rfl rfl
Rewards pledged

No rewards pledged yet.