Documentation

Mathlib.Data.Bool.Set

Booleans and set operations #

This file contains three 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 โ†’ ฮฑ) :
Set.range f = {f false, f true}
@[simp]
theorem Bool.compl_singleton (b : Bool) :
{b}แถœ = {!b}