# Indicator function valued in bool #

See also `Set.indicator` and `Set.piecewise`.

source
noncomputable def Set.boolIndicator {α : Type u_1} (s : Set α) (x : α) :
Bool

`boolIndicator` maps `x` to `true` if `x ∈ s`, else to `false`

Equations

- s.boolIndicator x = if x ∈ s then true else false

Instances For

source
theorem Set.mem_iff_boolIndicator {α : Type u_1} (s : Set α) (x : α) :
x ∈ s ↔ s.boolIndicator x = true
source
theorem Set.notMem_iff_boolIndicator {α : Type u_1} (s : Set α) (x : α) :
x ∉ s ↔ s.boolIndicator x = false
source
@[deprecated Set.notMem_iff_boolIndicator (since := "2025-05-23")]
theorem Set.not_mem_iff_boolIndicator {α : Type u_1} (s : Set α) (x : α) :
x ∉ s ↔ s.boolIndicator x = false

Alias of `Set.notMem_iff_boolIndicator`.

source
theorem Set.preimage_boolIndicator_true {α : Type u_1} (s : Set α) :
s.boolIndicator ⁻¹' {true} = s
source
theorem Set.preimage_boolIndicator_false {α : Type u_1} (s : Set α) :
s.boolIndicator ⁻¹' {false} = s ᶜ
source
theorem Set.preimage_boolIndicator_eq_union {α : Type u_1} (s : Set α) (t : Set Bool) :
s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then s ᶜ else ∅
source
theorem Set.preimage_boolIndicator {α : Type u_1} (s : Set α) (t : Set Bool) :
s.boolIndicator ⁻¹' t = univ ∨ s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = s ᶜ ∨ s.boolIndicator ⁻¹' t = ∅