mathlib3 documentation

data.set.bool_indicator

Indicator function valued in bool #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

See also set.indicator and set.piecewise.

source
noncomputable def set.bool_indicator {α : Type u_1} (s : set α) (x : α) :
bool

bool_indicator maps x to tt if x ∈ s, else to ff

Equations
source
theorem set.mem_iff_bool_indicator {α : Type u_1} (s : set α) (x : α) :
x ∈ s ↔ s.bool_indicator x = bool.tt
source
theorem set.not_mem_iff_bool_indicator {α : Type u_1} (s : set α) (x : α) :
x ∉ s ↔ s.bool_indicator x = bool.ff
source
theorem set.preimage_bool_indicator_tt {α : Type u_1} (s : set α) :
s.bool_indicator ⁻¹' {bool.tt} = s
source
theorem set.preimage_bool_indicator_ff {α : Type u_1} (s : set α) :
s.bool_indicator ⁻¹' {bool.ff} = sᶜ
source
theorem set.preimage_bool_indicator_eq_union {α : Type u_1} (s : set α) (t : set bool) :
s.bool_indicator ⁻¹' t = ite (bool.tt ∈ t) s ∅ ∪ ite (bool.ff ∈ t) sᶜ ∅
source
theorem set.preimage_bool_indicator {α : Type u_1} (s : set α) (t : set bool) :
s.bool_indicator ⁻¹' t = set.univ ∨ s.bool_indicator ⁻¹' t = s ∨ s.bool_indicator ⁻¹' t = sᶜ ∨ s.bool_indicator ⁻¹' t = ∅