Documentation

Mathlib.Logic.Equiv.Bool

Equivalences involving `Bool` #

This file shows that not : Bool → Bool is an equivalence and derives some consequences

def Equiv.boolNot :

Perm Bool

The boolean negation function not : Bool → Bool is an involution and thus an equivalence.

Instances For

@[simp]

theorem Equiv.boolNot_apply (a✝ : Bool) :

boolNot a✝ = !a✝

@[simp]

theorem Equiv.boolNot_symm_apply (a✝ : Bool) :

(Equiv.symm boolNot) a✝ = !a✝

theorem Bool.not_bijective :

Function.Bijective not

theorem Bool.not_injective :

Function.Injective not

theorem Bool.not_surjective :

Function.Surjective not

theorem Bool.not_leftInverse :

Function.LeftInverse not not

theorem Bool.not_rightInverse :

Function.RightInverse not not

theorem Bool.not_hasLeftInverse :

Function.HasLeftInverse not

theorem Bool.not_hasRightInverse :

Function.HasRightInverse not