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

• Set.boolIndicator s x = if x ∈ s then true else false

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

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

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

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

theorem Set.preimage_boolIndicator_eq_union {α : Type u_1} (s : Set α) (t : Set Bool) : Set.boolIndicator s ⁻¹' 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) : Set.boolIndicator s ⁻¹' t = Set.univ ∨ Set.boolIndicator s ⁻¹' t = s ∨ Set.boolIndicator s ⁻¹' t = sᶜ ∨ Set.boolIndicator s ⁻¹' t = ∅