mathlib3 documentation


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.

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

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

theorem set.mem_iff_bool_indicator {α : Type u_1} (s : set α) (x : α) :
theorem set.not_mem_iff_bool_indicator {α : Type u_1} (s : set α) (x : α) :