mathlib documentation

data.set.bool

Booleans and set operations #

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

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