Indicator function valued in bool

See also Set.indicator and Set.piecewise.

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

theorem Set.mem_iff_boolIndicator {α : Type u_1} (s : Set α) (x : α) : x ∈ s ↔ s.boolIndicator x = true

theorem Set.notMem_iff_boolIndicator {α : Type u_1} (s : Set α) (x : α) : ¬x ∈ s ↔ s.boolIndicator x = false

theorem Set.preimage_boolIndicator_true {α : Type u_1} (s : Set α) : s.boolIndicator ⁻¹' {true} = s

theorem Set.preimage_boolIndicator_false {α : Type u_1} (s : Set α) : s.boolIndicator ⁻¹' {false} = sᶜ

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 ∅

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 = ∅