Mathlib.Data.Bool.Set

Module docstring

{"# Booleans and set operations

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

Bool.univ_eq theorem

: (univ : Set Bool) = { false, true }

Full source

@[simp]
theorem univ_eq : (univ : Set Bool) = {false, true} :=
  (eq_univ_of_forall Bool.dichotomy).symm

Universal Set of Booleans Equals $\{\text{false}, \text{true}\}$

Informal description

The universal set of boolean values is equal to the set containing both `false` and `true`, i.e., $\text{univ} = \{\text{false}, \text{true}\}$.

Bool.range_eq theorem

{α : Type*} (f : Bool → α) : range f = {f false, f true}

Full source

@[simp]
theorem range_eq {α : Type*} (f : Bool → α) : range f = {f false, f true} := by
  rw [← image_univ, univ_eq, image_pair]

Range of a Boolean Function is $\{f(\text{false}), f(\text{true})\}$

Informal description

For any function $f$ from the boolean type to a type $\alpha$, the range of $f$ is equal to the set $\{f(\text{false}), f(\text{true})\}$.

Bool.compl_singleton theorem

(b : Bool) : ({ b }ᶜ : Set Bool) = {!b}

Full source

@[simp] theorem compl_singleton (b : Bool) : ({b}{b}ᶜ : Set Bool) = {!b} :=
  Set.ext fun _ => eq_not_iff.symm

Complement of a Boolean Singleton is its Negation

Informal description

For any boolean value $b$, the complement of the singleton set $\{b\}$ in the type of booleans is equal to the singleton set containing the negation of $b$, i.e., $\{b\}^c = \{\neg b\}$.