HepLean Documentation

Mathlib.Data.Bool.Set

Booleans and set operations #

This file contains two trivial lemmas about Bool, Set.univ, and Set.range.

@[simp]
theorem Bool.univ_eq :
Set.univ = {false, true}
@[simp]
theorem Bool.range_eq {α : Type u_1} (f : Boolα) :
@[simp]
theorem Bool.compl_singleton (b : Bool) :
{b} = {!b}