mathlib3 documentation

data.bool.set

Booleans and set operations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains two trivial lemmas about bool, set.univ, and set.range.

source
@[simp]
theorem bool.univ_eq  :
set.univ = {bool.ff, bool.tt}
source
@[simp]
theorem bool.range_eq {α : Type u_1} (f : bool → α) :
set.range f = {f bool.ff, f bool.tt}
source
@[simp]
theorem bool.compl_singleton (b : bool) :
{b}ᶜ = {!b}