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.
bool_indicator maps x to tt if x ∈ s, else to ff
theorem
set.mem_iff_bool_indicator
{α : Type u_1}
(s : set α)
(x : α) :
x ∈ s ↔ s.bool_indicator x = bool.tt
theorem
set.not_mem_iff_bool_indicator
{α : Type u_1}
(s : set α)
(x : α) :
x ∉ s ↔ s.bool_indicator x = bool.ff
theorem
set.preimage_bool_indicator_tt
{α : Type u_1}
(s : set α) :
s.bool_indicator ⁻¹' {bool.tt} = s
theorem
set.preimage_bool_indicator_ff
{α : Type u_1}
(s : set α) :
s.bool_indicator ⁻¹' {bool.ff} = sᶜ
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 = ∅