# Documentation

Mathlib.Algebra.IndicatorFunction

# Indicator function #

• Set.indicator (s : Set α) (f : α → β) (a : α) is f a if a ∈ s and is 0 otherwise.
• Set.mulIndicator (s : Set α) (f : α → β) (a : α) is f a if a ∈ s and is 1 otherwise.

## Implementation note #

In mathematics, an indicator function or a characteristic function is a function used to indicate membership of an element in a set s, having the value 1 for all elements of s and the value 0 otherwise. But since it is usually used to restrict a function to a certain set s, we let the indicator function take the value f x for some function f, instead of 1. If the usual indicator function is needed, just set f to be the constant function fun _ ↦ 1.

The indicator function is implemented non-computably, to avoid having to pass around Decidable arguments. This is in contrast with the design of Pi.single or Set.piecewise.

## Tags #

indicator, characteristic

noncomputable def Set.indicator {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : αM) (x : α) :
M

Set.indicator s f a is f a if a ∈ s, 0 otherwise.

Instances For
noncomputable def Set.mulIndicator {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (f : αM) (x : α) :
M

Set.mulIndicator s f a is f a if a ∈ s, 1 otherwise.

Instances For
@[simp]
theorem Set.piecewise_eq_indicator {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} [DecidablePred fun x => x s] :
=
@[simp]
theorem Set.piecewise_eq_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} [DecidablePred fun x => x s] :
=
theorem Set.indicator_apply {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : αM) (a : α) [Decidable (a s)] :
= if a s then f a else 0
theorem Set.mulIndicator_apply {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (f : αM) (a : α) [Decidable (a s)] :
= if a s then f a else 1
@[simp]
theorem Set.indicator_of_mem {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {a : α} (h : a s) (f : αM) :
= f a
@[simp]
theorem Set.mulIndicator_of_mem {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {a : α} (h : a s) (f : αM) :
= f a
@[simp]
theorem Set.indicator_of_not_mem {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {a : α} (h : ¬a s) (f : αM) :
= 0
@[simp]
theorem Set.mulIndicator_of_not_mem {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {a : α} (h : ¬a s) (f : αM) :
= 1
theorem Set.indicator_eq_zero_or_self {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : αM) (a : α) :
= 0 = f a
theorem Set.mulIndicator_eq_one_or_self {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (f : αM) (a : α) :
= 1 = f a
@[simp]
theorem Set.indicator_apply_eq_self {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {a : α} :
= f a ¬a sf a = 0
@[simp]
theorem Set.mulIndicator_apply_eq_self {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {a : α} :
= f a ¬a sf a = 1
@[simp]
theorem Set.indicator_eq_self {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} :
= f
@[simp]
theorem Set.mulIndicator_eq_self {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
= f
theorem Set.indicator_eq_self_of_superset {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {t : Set α} {f : αM} (h1 : = f) (h2 : s t) :
= f
theorem Set.mulIndicator_eq_self_of_superset {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {t : Set α} {f : αM} (h1 : = f) (h2 : s t) :
= f
@[simp]
theorem Set.indicator_apply_eq_zero {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {a : α} :
= 0 a sf a = 0
@[simp]
theorem Set.mulIndicator_apply_eq_one {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {a : α} :
= 1 a sf a = 1
@[simp]
theorem Set.indicator_eq_zero {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} :
( = fun x => 0)
@[simp]
theorem Set.mulIndicator_eq_one {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
( = fun x => 1)
@[simp]
theorem Set.indicator_eq_zero' {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} :
= 0
@[simp]
theorem Set.mulIndicator_eq_one' {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
= 1
theorem Set.indicator_apply_ne_zero {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {a : α} :
0 a
theorem Set.mulIndicator_apply_ne_one {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {a : α} :
1 a
@[simp]
theorem Set.support_indicator {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} :
=
@[simp]
theorem Set.mulSupport_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
theorem Set.mem_of_indicator_ne_zero {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {a : α} (h : 0) :
a s

If an additive indicator function is not equal to 0 at a point, then that point is in the set.

theorem Set.mem_of_mulIndicator_ne_one {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {a : α} (h : 1) :
a s

If a multiplicative indicator function is not equal to 1 at a point, then that point is in the set.

theorem Set.eqOn_indicator {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} :
Set.EqOn () f s
theorem Set.eqOn_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
Set.EqOn () f s
theorem Set.support_indicator_subset {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} :
s
theorem Set.mulSupport_mulIndicator_subset {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
@[simp]
theorem Set.indicator_support {α : Type u_1} {M : Type u_4} [Zero M] {f : αM} :
= f
@[simp]
theorem Set.mulIndicator_mulSupport {α : Type u_1} {M : Type u_4} [One M] {f : αM} :
@[simp]
theorem Set.indicator_range_comp {α : Type u_1} {M : Type u_4} [Zero M] {ι : Sort u_6} (f : ια) (g : αM) :
f = g f
@[simp]
theorem Set.mulIndicator_range_comp {α : Type u_1} {M : Type u_4} [One M] {ι : Sort u_6} (f : ια) (g : αM) :
f = g f
theorem Set.indicator_congr {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {g : αM} (h : Set.EqOn f g s) :
=
theorem Set.mulIndicator_congr {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {g : αM} (h : Set.EqOn f g s) :
@[simp]
theorem Set.indicator_univ {α : Type u_1} {M : Type u_4} [Zero M] (f : αM) :
Set.indicator Set.univ f = f
@[simp]
theorem Set.mulIndicator_univ {α : Type u_1} {M : Type u_4} [One M] (f : αM) :
Set.mulIndicator Set.univ f = f
@[simp]
theorem Set.indicator_empty {α : Type u_1} {M : Type u_4} [Zero M] (f : αM) :
= fun x => 0
@[simp]
theorem Set.mulIndicator_empty {α : Type u_1} {M : Type u_4} [One M] (f : αM) :
= fun x => 1
theorem Set.indicator_empty' {α : Type u_1} {M : Type u_4} [Zero M] (f : αM) :
= 0
theorem Set.mulIndicator_empty' {α : Type u_1} {M : Type u_4} [One M] (f : αM) :
@[simp]
theorem Set.indicator_zero {α : Type u_1} (M : Type u_4) [Zero M] (s : Set α) :
(Set.indicator s fun x => 0) = fun x => 0
@[simp]
theorem Set.mulIndicator_one {α : Type u_1} (M : Type u_4) [One M] (s : Set α) :
(Set.mulIndicator s fun x => 1) = fun x => 1
@[simp]
theorem Set.indicator_zero' {α : Type u_1} (M : Type u_4) [Zero M] {s : Set α} :
= 0
@[simp]
theorem Set.mulIndicator_one' {α : Type u_1} (M : Type u_4) [One M] {s : Set α} :
= 1
theorem Set.indicator_indicator {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (t : Set α) (f : αM) :
theorem Set.mulIndicator_mulIndicator {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (t : Set α) (f : αM) :
@[simp]
theorem Set.indicator_inter_support {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : αM) :
@[simp]
theorem Set.mulIndicator_inter_mulSupport {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (f : αM) :
=
theorem Set.comp_indicator {α : Type u_1} {β : Type u_2} {M : Type u_4} [Zero M] (h : Mβ) (f : αM) {s : Set α} {x : α} [DecidablePred fun x => x s] :
h () = Set.piecewise s (h f) (Function.const α (h 0)) x
theorem Set.comp_mulIndicator {α : Type u_1} {β : Type u_2} {M : Type u_4} [One M] (h : Mβ) (f : αM) {s : Set α} {x : α} [DecidablePred fun x => x s] :
h () = Set.piecewise s (h f) (Function.const α (h 1)) x
theorem Set.indicator_comp_right {α : Type u_1} {β : Type u_2} {M : Type u_4} [Zero M] {s : Set α} (f : βα) {g : αM} {x : β} :
Set.indicator (f ⁻¹' s) (g f) x = Set.indicator s g (f x)
theorem Set.mulIndicator_comp_right {α : Type u_1} {β : Type u_2} {M : Type u_4} [One M] {s : Set α} (f : βα) {g : αM} {x : β} :
Set.mulIndicator (f ⁻¹' s) (g f) x = Set.mulIndicator s g (f x)
theorem Set.indicator_image {α : Type u_1} {β : Type u_2} {M : Type u_4} [Zero M] {s : Set α} {f : βM} {g : αβ} (hg : ) {x : α} :
Set.indicator (g '' s) f (g x) = Set.indicator s (f g) x
theorem Set.mulIndicator_image {α : Type u_1} {β : Type u_2} {M : Type u_4} [One M] {s : Set α} {f : βM} {g : αβ} (hg : ) {x : α} :
Set.mulIndicator (g '' s) f (g x) = Set.mulIndicator s (f g) x
theorem Set.indicator_comp_of_zero {α : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] {s : Set α} {f : αM} {g : MN} (hg : g 0 = 0) :
Set.indicator s (g f) = g
theorem Set.mulIndicator_comp_of_one {α : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] {s : Set α} {f : αM} {g : MN} (hg : g 1 = 1) :
theorem Set.comp_indicator_const {α : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] {s : Set α} (c : M) (f : MN) (hf : f 0 = 0) :
(fun x => f (Set.indicator s (fun x => c) x)) = Set.indicator s fun x => f c
theorem Set.comp_mulIndicator_const {α : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] {s : Set α} (c : M) (f : MN) (hf : f 1 = 1) :
(fun x => f (Set.mulIndicator s (fun x => c) x)) = Set.mulIndicator s fun x => f c
theorem Set.indicator_preimage {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : αM) (B : Set M) :
⁻¹' B = Set.ite s (f ⁻¹' B) (0 ⁻¹' B)
theorem Set.mulIndicator_preimage {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (f : αM) (B : Set M) :
⁻¹' B = Set.ite s (f ⁻¹' B) (1 ⁻¹' B)
theorem Set.indicator_zero_preimage {α : Type u_1} {M : Type u_4} [Zero M] {t : Set α} (s : Set M) :
⁻¹' s {Set.univ, }
theorem Set.mulIndicator_one_preimage {α : Type u_1} {M : Type u_4} [One M] {t : Set α} (s : Set M) :
⁻¹' s {Set.univ, }
theorem Set.indicator_const_preimage_eq_union {α : Type u_1} {M : Type u_4} [Zero M] (U : Set α) (s : Set M) (a : M) [Decidable (a s)] [Decidable (0 s)] :
(Set.indicator U fun x => a) ⁻¹' s = (if a s then U else ) if 0 s then U else
theorem Set.mulIndicator_const_preimage_eq_union {α : Type u_1} {M : Type u_4} [One M] (U : Set α) (s : Set M) (a : M) [Decidable (a s)] [Decidable (1 s)] :
(Set.mulIndicator U fun x => a) ⁻¹' s = (if a s then U else ) if 1 s then U else
theorem Set.indicator_const_preimage {α : Type u_1} {M : Type u_4} [Zero M] (U : Set α) (s : Set M) (a : M) :
(Set.indicator U fun x => a) ⁻¹' s {Set.univ, U, U, }
theorem Set.mulIndicator_const_preimage {α : Type u_1} {M : Type u_4} [One M] (U : Set α) (s : Set M) (a : M) :
(Set.mulIndicator U fun x => a) ⁻¹' s {Set.univ, U, U, }
theorem Set.indicator_one_preimage {α : Type u_1} {M : Type u_4} [One M] [Zero M] (U : Set α) (s : Set M) :
⁻¹' s {Set.univ, U, U, }
theorem Set.indicator_preimage_of_not_mem {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : αM) {t : Set M} (ht : ¬0 t) :
⁻¹' t = f ⁻¹' t s
theorem Set.mulIndicator_preimage_of_not_mem {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (f : αM) {t : Set M} (ht : ¬1 t) :
⁻¹' t = f ⁻¹' t s
theorem Set.mem_range_indicator {α : Type u_1} {M : Type u_4} [Zero M] {r : M} {s : Set α} {f : αM} :
r Set.range () r = 0 s Set.univ r f '' s
theorem Set.mem_range_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {r : M} {s : Set α} {f : αM} :
r r = 1 s Set.univ r f '' s
theorem Set.indicator_rel_indicator {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {g : αM} {a : α} {r : MMProp} (h1 : r 0 0) (ha : a sr (f a) (g a)) :
r () ()
theorem Set.mulIndicator_rel_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {g : αM} {a : α} {r : MMProp} (h1 : r 1 1) (ha : a sr (f a) (g a)) :
r () ()
theorem Set.indicator_union_add_inter_apply {α : Type u_1} {M : Type u_4} [] (f : αM) (s : Set α) (t : Set α) (a : α) :
Set.indicator (s t) f a + Set.indicator (s t) f a = +
theorem Set.mulIndicator_union_mul_inter_apply {α : Type u_1} {M : Type u_4} [] (f : αM) (s : Set α) (t : Set α) (a : α) :
theorem Set.indicator_union_add_inter {α : Type u_1} {M : Type u_4} [] (f : αM) (s : Set α) (t : Set α) :
theorem Set.mulIndicator_union_mul_inter {α : Type u_1} {M : Type u_4} [] (f : αM) (s : Set α) (t : Set α) :
theorem Set.indicator_union_of_not_mem_inter {α : Type u_1} {M : Type u_4} [] {s : Set α} {t : Set α} {a : α} (h : ¬a s t) (f : αM) :
Set.indicator (s t) f a = +
theorem Set.mulIndicator_union_of_not_mem_inter {α : Type u_1} {M : Type u_4} [] {s : Set α} {t : Set α} {a : α} (h : ¬a s t) (f : αM) :
Set.mulIndicator (s t) f a = *
theorem Set.indicator_union_of_disjoint {α : Type u_1} {M : Type u_4} [] {s : Set α} {t : Set α} (h : Disjoint s t) (f : αM) :
Set.indicator (s t) f = fun a => +
theorem Set.mulIndicator_union_of_disjoint {α : Type u_1} {M : Type u_4} [] {s : Set α} {t : Set α} (h : Disjoint s t) (f : αM) :
Set.mulIndicator (s t) f = fun a => *
theorem Set.indicator_symmDiff {α : Type u_1} {M : Type u_4} [] (s : Set α) (t : Set α) (f : αM) :
Set.indicator (s t) f = Set.indicator (s \ t) f + Set.indicator (t \ s) f
theorem Set.mulIndicator_symmDiff {α : Type u_1} {M : Type u_4} [] (s : Set α) (t : Set α) (f : αM) :
theorem Set.indicator_add {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (g : αM) :
(Set.indicator s fun a => f a + g a) = fun a => +
theorem Set.mulIndicator_mul {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (g : αM) :
(Set.mulIndicator s fun a => f a * g a) = fun a => *
theorem Set.indicator_add' {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (g : αM) :
Set.indicator s (f + g) = +
theorem Set.mulIndicator_mul' {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (g : αM) :
@[simp]
theorem Set.indicator_compl_add_self_apply {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (a : α) :
+ = f a
@[simp]
theorem Set.mulIndicator_compl_mul_self_apply {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (a : α) :
* = f a
@[simp]
theorem Set.indicator_compl_add_self {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) :
+ = f
@[simp]
theorem Set.mulIndicator_compl_mul_self {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) :
= f
@[simp]
theorem Set.indicator_self_add_compl_apply {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (a : α) :
+ = f a
@[simp]
theorem Set.mulIndicator_self_mul_compl_apply {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (a : α) :
* = f a
@[simp]
theorem Set.indicator_self_add_compl {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) :
+ = f
@[simp]
theorem Set.mulIndicator_self_mul_compl {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) :
= f
theorem Set.indicator_add_eq_left {α : Type u_1} {M : Type u_4} [] {f : αM} {g : αM} (h : ) :
Set.indicator () (f + g) = f
theorem Set.mulIndicator_mul_eq_left {α : Type u_1} {M : Type u_4} [] {f : αM} {g : αM} (h : ) :
Set.mulIndicator () (f * g) = f
theorem Set.indicator_add_eq_right {α : Type u_1} {M : Type u_4} [] {f : αM} {g : αM} (h : ) :
Set.indicator () (f + g) = g
theorem Set.mulIndicator_mul_eq_right {α : Type u_1} {M : Type u_4} [] {f : αM} {g : αM} (h : ) :
Set.mulIndicator () (f * g) = g
theorem Set.indicator_add_compl_eq_piecewise {α : Type u_1} {M : Type u_4} [] {s : Set α} [DecidablePred fun x => x s] (f : αM) (g : αM) :
+ =
theorem Set.mulIndicator_mul_compl_eq_piecewise {α : Type u_1} {M : Type u_4} [] {s : Set α} [DecidablePred fun x => x s] (f : αM) (g : αM) :
=
theorem Set.indicatorHom.proof_1 {α : Type u_1} (M : Type u_2) [] (s : Set α) :
(Set.indicator s fun x => 0) = fun x => 0
noncomputable def Set.indicatorHom {α : Type u_6} (M : Type u_7) [] (s : Set α) :
(αM) →+ αM

Set.indicator as an addMonoidHom.

Instances For
noncomputable def Set.mulIndicatorHom {α : Type u_6} (M : Type u_7) [] (s : Set α) :
(αM) →* αM

Set.mulIndicator as a monoidHom.

Instances For
theorem Set.indicator_smul_apply {α : Type u_1} {M : Type u_4} {A : Type u_6} [] [] [] (s : Set α) (r : αM) (f : αA) (x : α) :
Set.indicator s (fun x => r x f x) x = r x
theorem Set.indicator_smul {α : Type u_1} {M : Type u_4} {A : Type u_6} [] [] [] (s : Set α) (r : αM) (f : αA) :
(Set.indicator s fun x => r x f x) = fun x => r x
theorem Set.indicator_const_smul_apply {α : Type u_1} {M : Type u_4} {A : Type u_6} [] [] [] (s : Set α) (r : M) (f : αA) (x : α) :
Set.indicator s (fun x => r f x) x = r
theorem Set.indicator_const_smul {α : Type u_1} {M : Type u_4} {A : Type u_6} [] [] [] (s : Set α) (r : M) (f : αA) :
(Set.indicator s fun x => r f x) = fun x => r
theorem Set.indicator_smul_apply_left {α : Type u_1} {M : Type u_4} {A : Type u_6} [Zero A] [Zero M] [] (s : Set α) (r : αM) (f : αA) (x : α) :
Set.indicator s (fun x => r x f x) x = f x
theorem Set.indicator_smul_left {α : Type u_1} {M : Type u_4} {A : Type u_6} [Zero A] [Zero M] [] (s : Set α) (r : αM) (f : αA) :
(Set.indicator s fun x => r x f x) = fun x => f x
theorem Set.indicator_smul_const_apply {α : Type u_1} {M : Type u_4} {A : Type u_6} [Zero A] [Zero M] [] (s : Set α) (r : αM) (a : A) (x : α) :
Set.indicator s (fun x => r x a) x = a
theorem Set.indicator_smul_const {α : Type u_1} {M : Type u_4} {A : Type u_6} [Zero A] [Zero M] [] (s : Set α) (r : αM) (a : A) :
(Set.indicator s fun x => r x a) = fun x => a
theorem Set.indicator_neg' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
theorem Set.mulIndicator_inv' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
= ()⁻¹
theorem Set.indicator_neg {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
(Set.indicator s fun a => -f a) = fun a => -
theorem Set.mulIndicator_inv {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
(Set.mulIndicator s fun a => (f a)⁻¹) = fun a => ()⁻¹
theorem Set.indicator_sub {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) (g : αG) :
(Set.indicator s fun a => f a - g a) = fun a => -
theorem Set.mulIndicator_div {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) (g : αG) :
(Set.mulIndicator s fun a => f a / g a) = fun a => /
theorem Set.indicator_sub' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) (g : αG) :
Set.indicator s (f - g) = -
theorem Set.mulIndicator_div' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) (g : αG) :
theorem Set.indicator_compl' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
= f + -
theorem Set.mulIndicator_compl {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
= f * ()⁻¹
theorem Set.indicator_compl {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
= f -
theorem Set.mulIndicator_compl' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
= f /
theorem Set.indicator_diff' {α : Type u_1} {G : Type u_6} [] {s : Set α} {t : Set α} (h : s t) (f : αG) :
Set.indicator (t \ s) f = + -
theorem Set.mulIndicator_diff {α : Type u_1} {G : Type u_6} [] {s : Set α} {t : Set α} (h : s t) (f : αG) :
theorem Set.indicator_diff {α : Type u_1} {G : Type u_6} [] {s : Set α} {t : Set α} (h : s t) (f : αG) :
Set.indicator (t \ s) f = -
theorem Set.mulIndicator_diff' {α : Type u_1} {G : Type u_6} [] {s : Set α} {t : Set α} (h : s t) (f : αG) :
theorem Set.apply_indicator_symmDiff {α : Type u_1} {β : Type u_2} {G : Type u_6} [] {g : Gβ} (hg : ∀ (x : G), g (-x) = g x) (s : Set α) (t : Set α) (f : αG) (x : α) :
g (Set.indicator (s t) f x) = g ( - )
theorem Set.apply_mulIndicator_symmDiff {α : Type u_1} {β : Type u_2} {G : Type u_6} [] {g : Gβ} (hg : ∀ (x : G), g x⁻¹ = g x) (s : Set α) (t : Set α) (f : αG) (x : α) :
g (Set.mulIndicator (s t) f x) = g ( / )
theorem Set.abs_indicator_symmDiff {α : Type u_1} {G : Type u_6} (s : Set α) (t : Set α) (f : αG) (x : α) :
|Set.indicator (s t) f x| = | - |
theorem Set.sum_indicator_subset_of_eq_zero {α : Type u_1} {M : Type u_4} {N : Type u_5} [] [Zero N] (f : αN) (g : αNM) {s : } {t : } (h : s t) (hg : ∀ (a : α), g a 0 = 0) :
(Finset.sum s fun i => g i (f i)) = Finset.sum t fun i => g i (Set.indicator (s) f i)

Consider a sum of g i (f i) over a Finset. Suppose g is a function such as multiplication, which maps a second argument of 0 to 0. (A typical use case would be a weighted sum of f i * h i or f i • h i, where f gives the weights that are multiplied by some other function h.) Then if f is replaced by the corresponding indicator function, the Finset may be replaced by a possibly larger Finset without changing the value of the sum.

theorem Set.prod_mulIndicator_subset_of_eq_one {α : Type u_1} {M : Type u_4} {N : Type u_5} [] [One N] (f : αN) (g : αNM) {s : } {t : } (h : s t) (hg : ∀ (a : α), g a 1 = 1) :
(Finset.prod s fun i => g i (f i)) = Finset.prod t fun i => g i (Set.mulIndicator (s) f i)

Consider a product of g i (f i) over a Finset. Suppose g is a function such as Pow, which maps a second argument of 1 to 1. Then if f is replaced by the corresponding multiplicative indicator function, the Finset may be replaced by a possibly larger Finset without changing the value of the sum.

theorem Set.sum_indicator_subset {α : Type u_1} {M : Type u_4} [] (f : αM) {s : } {t : } (h : s t) :
(Finset.sum s fun i => f i) = Finset.sum t fun i => Set.indicator (s) f i

Summing an indicator function over a possibly larger Finset is the same as summing the original function over the original finset.

theorem Set.prod_mulIndicator_subset {α : Type u_1} {M : Type u_4} [] (f : αM) {s : } {t : } (h : s t) :
(Finset.prod s fun i => f i) = Finset.prod t fun i => Set.mulIndicator (s) f i

Taking the product of an indicator function over a possibly larger Finset is the same as taking the original function over the original Finset.

theorem Finset.sum_indicator_eq_sum_filter {α : Type u_1} {ι : Type u_3} {M : Type u_4} [] (s : ) (f : ιαM) (t : ιSet α) (g : ια) [DecidablePred fun i => g i t i] :
(Finset.sum s fun i => Set.indicator (t i) (f i) (g i)) = Finset.sum (Finset.filter (fun i => g i t i) s) fun i => f i (g i)
theorem Finset.prod_mulIndicator_eq_prod_filter {α : Type u_1} {ι : Type u_3} {M : Type u_4} [] (s : ) (f : ιαM) (t : ιSet α) (g : ια) [DecidablePred fun i => g i t i] :
(Finset.prod s fun i => Set.mulIndicator (t i) (f i) (g i)) = Finset.prod (Finset.filter (fun i => g i t i) s) fun i => f i (g i)
theorem Set.indicator_finset_sum {α : Type u_1} {ι : Type u_3} {M : Type u_4} [] (I : ) (s : Set α) (f : ιαM) :
Set.indicator s (Finset.sum I fun i => f i) = Finset.sum I fun i => Set.indicator s (f i)
theorem Set.mulIndicator_finset_prod {α : Type u_1} {ι : Type u_3} {M : Type u_4} [] (I : ) (s : Set α) (f : ιαM) :
Set.mulIndicator s (Finset.prod I fun i => f i) = Finset.prod I fun i => Set.mulIndicator s (f i)
theorem Set.indicator_finset_biUnion {α : Type u_1} {ι : Type u_3} {M : Type u_4} [] (I : ) (s : ιSet α) {f : αM} :
(∀ (i : ι), i I∀ (j : ι), j Ii jDisjoint (s i) (s j)) → Set.indicator (⋃ (i : ι) (_ : i I), s i) f = fun a => Finset.sum I fun i => Set.indicator (s i) f a
theorem Set.mulIndicator_finset_biUnion {α : Type u_1} {ι : Type u_3} {M : Type u_4} [] (I : ) (s : ιSet α) {f : αM} :
(∀ (i : ι), i I∀ (j : ι), j Ii jDisjoint (s i) (s j)) → Set.mulIndicator (⋃ (i : ι) (_ : i I), s i) f = fun a => Finset.prod I fun i => Set.mulIndicator (s i) f a
theorem Set.indicator_finset_biUnion_apply {α : Type u_1} {ι : Type u_3} {M : Type u_4} [] (I : ) (s : ιSet α) {f : αM} (h : ∀ (i : ι), i I∀ (j : ι), j Ii jDisjoint (s i) (s j)) (x : α) :
Set.indicator (⋃ (i : ι) (_ : i I), s i) f x = Finset.sum I fun i => Set.indicator (s i) f x
theorem Set.mulIndicator_finset_biUnion_apply {α : Type u_1} {ι : Type u_3} {M : Type u_4} [] (I : ) (s : ιSet α) {f : αM} (h : ∀ (i : ι), i I∀ (j : ι), j Ii jDisjoint (s i) (s j)) (x : α) :
Set.mulIndicator (⋃ (i : ι) (_ : i I), s i) f x = Finset.prod I fun i => Set.mulIndicator (s i) f x
theorem Set.indicator_mul {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (g : αM) :
(Set.indicator s fun a => f a * g a) = fun a => *
theorem Set.indicator_mul_left {α : Type u_1} {M : Type u_4} [] {a : α} (s : Set α) (f : αM) (g : αM) :
Set.indicator s (fun a => f a * g a) a = * g a
theorem Set.indicator_mul_right {α : Type u_1} {M : Type u_4} [] {a : α} (s : Set α) (f : αM) (g : αM) :
Set.indicator s (fun a => f a * g a) a = f a *
theorem Set.inter_indicator_mul {α : Type u_1} {M : Type u_4} [] {t1 : Set α} {t2 : Set α} (f : αM) (g : αM) (x : α) :
Set.indicator (t1 t2) (fun x => f x * g x) x = Set.indicator t1 f x * Set.indicator t2 g x
theorem Set.inter_indicator_one {α : Type u_1} {M : Type u_4} [] {s : Set α} {t : Set α} :
Set.indicator (s t) 1 = *
theorem Set.indicator_prod_one {α : Type u_1} {β : Type u_2} {M : Type u_4} [] {s : Set α} {t : Set β} {x : α} {y : β} :
Set.indicator (s ×ˢ t) 1 (x, y) = *
theorem Set.indicator_eq_zero_iff_not_mem {α : Type u_1} (M : Type u_4) [] [] {U : Set α} {x : α} :
= 0 ¬x U
theorem Set.indicator_eq_one_iff_mem {α : Type u_1} (M : Type u_4) [] [] {U : Set α} {x : α} :
= 1 x U
theorem Set.indicator_one_inj {α : Type u_1} (M : Type u_4) [] [] {U : Set α} {V : Set α} (h : = ) :
U = V
theorem Set.indicator_apply_le' {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {a : α} {y : M} [LE M] (hfg : a sf a y) (hg : ¬a s0 y) :
y
theorem Set.mulIndicator_apply_le' {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {a : α} {y : M} [LE M] (hfg : a sf a y) (hg : ¬a s1 y) :
y
theorem Set.indicator_le' {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {g : αM} [LE M] (hfg : ∀ (a : α), a sf a g a) (hg : ∀ (a : α), ¬a s0 g a) :
g
theorem Set.mulIndicator_le' {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {g : αM} [LE M] (hfg : ∀ (a : α), a sf a g a) (hg : ∀ (a : α), ¬a s1 g a) :
g
theorem Set.le_indicator_apply {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {g : αM} {a : α} [LE M] {y : M} (hfg : a sy g a) (hf : ¬a sy 0) :
y
theorem Set.le_mulIndicator_apply {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {g : αM} {a : α} [LE M] {y : M} (hfg : a sy g a) (hf : ¬a sy 1) :
y
theorem Set.le_indicator {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {g : αM} [LE M] (hfg : ∀ (a : α), a sf a g a) (hf : ∀ (a : α), ¬a sf a 0) :
f
theorem Set.le_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {g : αM} [LE M] (hfg : ∀ (a : α), a sf a g a) (hf : ∀ (a : α), ¬a sf a 1) :
f
theorem Set.indicator_apply_nonneg {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {a : α} [] (h : a s0 f a) :
0
theorem Set.one_le_mulIndicator_apply {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {a : α} [] (h : a s1 f a) :
1
theorem Set.indicator_nonneg {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} [] (h : ∀ (a : α), a s0 f a) (a : α) :
0
theorem Set.one_le_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} [] (h : ∀ (a : α), a s1 f a) (a : α) :
1
theorem Set.indicator_apply_nonpos {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {a : α} [] (h : a sf a 0) :
0
theorem Set.mulIndicator_apply_le_one {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {a : α} [] (h : a sf a 1) :
1
theorem Set.indicator_nonpos {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} [] (h : ∀ (a : α), a sf a 0) (a : α) :
0
theorem Set.mulIndicator_le_one {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} [] (h : ∀ (a : α), a sf a 1) (a : α) :
1
theorem Set.indicator_le_indicator {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {g : αM} {a : α} [] (h : f a g a) :
theorem Set.mulIndicator_le_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {g : αM} {a : α} [] (h : f a g a) :
theorem Set.indicator_le_indicator_of_subset {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {t : Set α} {f : αM} [] (h : s t) (hf : ∀ (a : α), 0 f a) (a : α) :
theorem Set.mulIndicator_le_mulIndicator_of_subset {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {t : Set α} {f : αM} [] (h : s t) (hf : ∀ (a : α), 1 f a) (a : α) :
theorem Set.indicator_le_self' {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} [] (hf : ∀ (x : α), ¬x s0 f x) :
f
theorem Set.mulIndicator_le_self' {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} [] (hf : ∀ (x : α), ¬x s1 f x) :
f
theorem Set.indicator_iUnion_apply {α : Type u_1} {ι : Sort u_6} {M : Type u_7} [] [Zero M] (h1 : = 0) (s : ιSet α) (f : αM) (x : α) :
Set.indicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), Set.indicator (s i) f x
theorem Set.mulIndicator_iUnion_apply {α : Type u_1} {ι : Sort u_6} {M : Type u_7} [] [One M] (h1 : = 1) (s : ιSet α) (f : αM) (x : α) :
Set.mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), Set.mulIndicator (s i) f x
theorem Set.indicator_iInter_apply {α : Type u_1} {ι : Sort u_6} {M : Type u_7} [] [] [Zero M] (h1 : = 0) (s : ιSet α) (f : αM) (x : α) :
Set.indicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), Set.indicator (s i) f x
theorem Set.mulIndicator_iInter_apply {α : Type u_1} {ι : Sort u_6} {M : Type u_7} [] [] [One M] (h1 : = 1) (s : ιSet α) (f : αM) (x : α) :
Set.mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), Set.mulIndicator (s i) f x
theorem Set.indicator_le_self {α : Type u_1} {M : Type u_4} (s : Set α) (f : αM) :
f
theorem Set.mulIndicator_le_self {α : Type u_1} {M : Type u_4} (s : Set α) (f : αM) :
f
theorem Set.indicator_apply_le {α : Type u_1} {M : Type u_4} {a : α} {s : Set α} {f : αM} {g : αM} (hfg : a sf a g a) :
g a
theorem Set.mulIndicator_apply_le {α : Type u_1} {M : Type u_4} {a : α} {s : Set α} {f : αM} {g : αM} (hfg : a sf a g a) :
g a
theorem Set.indicator_le {α : Type u_1} {M : Type u_4} {s : Set α} {f : αM} {g : αM} (hfg : ∀ (a : α), a sf a g a) :
g
theorem Set.mulIndicator_le {α : Type u_1} {M : Type u_4} {s : Set α} {f : αM} {g : αM} (hfg : ∀ (a : α), a sf a g a) :
g
theorem Set.indicator_le_indicator_nonneg {α : Type u_1} {β : Type u_6} [] [Zero β] (s : Set α) (f : αβ) :
Set.indicator {x | 0 f x} f
theorem Set.indicator_nonpos_le_indicator {α : Type u_1} {β : Type u_6} [] [Zero β] (s : Set α) (f : αβ) :
Set.indicator {x | f x 0} f
theorem AddMonoidHom.map_indicator {α : Type u_1} {M : Type u_6} {N : Type u_7} [] [] (f : M →+ N) (s : Set α) (g : αM) (x : α) :
f () = Set.indicator s (f g) x
theorem MonoidHom.map_mulIndicator {α : Type u_1} {M : Type u_6} {N : Type u_7} [] [] (f : M →* N) (s : Set α) (g : αM) (x : α) :
f () = Set.mulIndicator s (f g) x