# 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.

Equations
• = if x s then f x else 0
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.

Equations
• = if x s then f x else 1
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 : as) (f : αM) :
= 0
@[simp]
theorem Set.mulIndicator_of_not_mem {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {a : α} (h : as) (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 asf 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 asf 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 : 0t) :
⁻¹' 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 : 1t) :
⁻¹' 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 : as 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 : as 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) :
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 : ) :
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 : ) :
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) :
=
noncomputable def Set.indicatorHom {α : Type u_6} (M : Type u_7) [] (s : Set α) :
(αM) →+ αM

Set.indicator as an addMonoidHom.

Equations
• = { toZeroHom := { toFun := , map_zero' := }, map_add' := }
Instances For
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.mulIndicatorHom {α : Type u_6} (M : Type u_7) [] (s : Set α) :
(αM) →* αM

Set.mulIndicator as a monoidHom.

Equations
• = { toOneHom := { toFun := , map_one' := }, map_mul' := }
Instances For
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 (symmDiff 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 (symmDiff s t) f x) = g ( / )
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 xU
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 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