Commit 2025-10-29 00:04 c1f64613

View on Github →

Feat(Logic): basic properties of boolean negation (#31028) We show that not : Bool -> Bool is an involutive equivalence and derive some immediate consequences.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Equiv/Bool.lean

added theorem Bool.not_bijective

added theorem Bool.not_hasLeftInverse

added theorem Bool.not_hasRightInverse

added theorem Bool.not_injective

added theorem Bool.not_leftInverse

added theorem Bool.not_rightInverse

added theorem Bool.not_surjective

added def Equiv.boolNot