Mathlib.Data.Set.BoolIndicator

Set.boolIndicator definition

(x : α)

Full source

/-- `boolIndicator` maps `x` to `true` if `x ∈ s`, else to `false` -/
noncomputable def boolIndicator (x : α) :=
  @ite _ (x ∈ s) (Classical.propDecidable _) true false

Boolean indicator function of a set

Informal description

The boolean indicator function of a set $s$ in a type $\alpha$ is defined as the function that maps an element $x \in \alpha$ to `true` if $x$ belongs to $s$, and to `false` otherwise.

Set.mem_iff_boolIndicator theorem

(x : α) : x ∈ s ↔ s.boolIndicator x = true

Full source

theorem mem_iff_boolIndicator (x : α) : x ∈ sx ∈ s ↔ s.boolIndicator x = true := by
  unfold boolIndicator
  split_ifs with h <;> simp [h]

Membership Criterion via Boolean Indicator Function

Informal description

For any element $x$ of type $\alpha$ and any set $s$ in $\alpha$, the element $x$ belongs to $s$ if and only if the boolean indicator function of $s$ evaluated at $x$ is `true`, i.e., $x \in s \leftrightarrow s.\mathrm{boolIndicator}(x) = \mathrm{true}$.

Set.not_mem_iff_boolIndicator theorem

(x : α) : x ∉ s ↔ s.boolIndicator x = false

Full source

theorem not_mem_iff_boolIndicator (x : α) : x ∉ sx ∉ s ↔ s.boolIndicator x = false := by
  unfold boolIndicator
  split_ifs with h <;> simp [h]

Non-membership Criterion via Boolean Indicator Function

Informal description

For any element $x$ of type $\alpha$ and any set $s$ in $\alpha$, the element $x$ does not belong to $s$ if and only if the boolean indicator function of $s$ evaluated at $x$ is `false`, i.e., $x \notin s \leftrightarrow s.\mathrm{boolIndicator}(x) = \mathrm{false}$.

Set.preimage_boolIndicator_true theorem

: s.boolIndicator ⁻¹' { true } = s

Full source

theorem preimage_boolIndicator_true : s.boolIndicator ⁻¹' {true} = s :=
  ext fun x ↦ (s.mem_iff_boolIndicator x).symm

Preimage of True under Boolean Indicator Function Equals Original Set

Informal description

For any set $s$ in a type $\alpha$, the preimage of the boolean indicator function of $s$ under the singleton set $\{\mathrm{true}\}$ is equal to $s$ itself, i.e., $s.\mathrm{boolIndicator}^{-1}(\{\mathrm{true}\}) = s$.

Set.preimage_boolIndicator_false theorem

: s.boolIndicator ⁻¹' { false } = sᶜ

Full source

theorem preimage_boolIndicator_false : s.boolIndicator ⁻¹' {false} = sᶜ :=
  ext fun x ↦ (s.not_mem_iff_boolIndicator x).symm

Preimage of False under Boolean Indicator Function Equals Complement of Set

Informal description

For any set $s$ in a type $\alpha$, the preimage of the singleton set $\{\mathrm{false}\}$ under the boolean indicator function of $s$ is equal to the complement of $s$, i.e., $s.\mathrm{boolIndicator}^{-1}(\{\mathrm{false}\}) = s^c$.

Set.preimage_boolIndicator_eq_union theorem

(t : Set Bool) : s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Full source

theorem preimage_boolIndicator_eq_union (t : Set Bool) :
    s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅ := by
  ext x
  simp only [boolIndicator, mem_preimage]
  split_ifs <;> simp [*]

Preimage of Boolean Indicator Function as Union of Set and Complement

Informal description

For any set $s$ in a type $\alpha$ and any subset $t$ of the boolean values $\{\mathrm{true}, \mathrm{false}\}$, the preimage of $t$ under the boolean indicator function of $s$ is equal to the union of: - $s$ if $\mathrm{true} \in t$, otherwise the empty set, and - the complement $s^c$ if $\mathrm{false} \in t$, otherwise the empty set. In other words, $s.\mathrm{boolIndicator}^{-1}(t) = (\text{if } \mathrm{true} \in t \text{ then } s \text{ else } \emptyset) \cup (\text{if } \mathrm{false} \in t \text{ then } s^c \text{ else } \emptyset)$.

Set.preimage_boolIndicator theorem

 (t : Set Bool) :
  s.boolIndicator ⁻¹' t = univ ∨ s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅

Full source

theorem preimage_boolIndicator (t : Set Bool) :
    s.boolIndicator ⁻¹' ts.boolIndicator ⁻¹' t = univ ∨
      s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅ := by
  simp only [preimage_boolIndicator_eq_union]
  split_ifs <;> simp [s.union_compl_self]

Possible Preimages of Boolean Indicator Function

Informal description

For any set $s$ in a type $\alpha$ and any subset $t$ of the boolean values $\{\mathrm{true}, \mathrm{false}\}$, the preimage of $t$ under the boolean indicator function of $s$ is equal to one of the following: - the universal set $\mathrm{univ}$, - the set $s$ itself, - the complement $s^c$ of $s$, or - the empty set $\emptyset$. In other words, $s.\mathrm{boolIndicator}^{-1}(t) \in \{\mathrm{univ}, s, s^c, \emptyset\}$.