Feat(Logic): basic properties of boolean negation (#31028)

We show that `not : Bool -> Bool` is an involutive equivalence and derive some immediate consequences.

Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Wrenna Robson <wren.robson@gmail.com>

Author: 3 people

Mathlib.lean

@@ -4533,6 +4533,7 @@ import Mathlib.Logic.Encodable.Lattice
 import Mathlib.Logic.Encodable.Pi
 import Mathlib.Logic.Equiv.Array
 import Mathlib.Logic.Equiv.Basic
+import Mathlib.Logic.Equiv.Bool
 import Mathlib.Logic.Equiv.Defs
 import Mathlib.Logic.Equiv.Embedding
 import Mathlib.Logic.Equiv.Fin.Basic

Mathlib/Logic/Equiv/Bool.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2025 Emily Riehl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Emily Riehl, Wrenna Robson
+-/
+import Mathlib.Logic.Equiv.Basic
+import Mathlib.Logic.Function.Basic
+
+/-!
+# Equivalences involving `Bool`
+
+This file shows that `not : Bool → Bool` is an equivalence and derives some consequences
+-/
+
+/-- The boolean negation function `not : Bool → Bool` is an involution and thus an equivalence. -/
+@[simps!]
+def Equiv.boolNot : Equiv.Perm Bool := Bool.involutive_not.toPerm
+
+namespace Bool
+
+open Function
+
+theorem not_bijective : Bijective not := Equiv.boolNot.bijective
+theorem not_injective : Injective not := Equiv.boolNot.injective
+theorem not_surjective : Surjective not := Equiv.boolNot.surjective
+
+theorem not_leftInverse : LeftInverse not not := not_not
+theorem not_rightInverse : RightInverse not not := not_not
+
+theorem not_hasLeftInverse : HasLeftInverse not := ⟨not, not_leftInverse⟩
+theorem not_hasRightInverse : HasRightInverse not := ⟨not, not_rightInverse⟩
+
+end Bool