# 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
• s.indicator f x = 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
• s.mulIndicator f x = 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] :
s.piecewise f 0 = s.indicator f
@[simp]
theorem Set.piecewise_eq_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} [DecidablePred fun (x : α) => x s] :
s.piecewise f 1 = s.mulIndicator f
theorem Set.indicator_apply {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : αM) (a : α) [Decidable (a s)] :
s.indicator f a = 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)] :
s.mulIndicator f a = 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) :
s.indicator f a = 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) :
s.mulIndicator f a = 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) :
s.indicator f a = 0
@[simp]
theorem Set.mulIndicator_of_not_mem {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {a : α} (h : as) (f : αM) :
s.mulIndicator f a = 1
theorem Set.indicator_eq_zero_or_self {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : αM) (a : α) :
s.indicator f a = 0 s.indicator f a = f a
theorem Set.mulIndicator_eq_one_or_self {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (f : αM) (a : α) :
s.mulIndicator f a = 1 s.mulIndicator f a = f a
@[simp]
theorem Set.indicator_apply_eq_self {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {a : α} :
s.indicator f 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 : α} :
s.mulIndicator f 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} :
s.indicator f = f
@[simp]
theorem Set.mulIndicator_eq_self {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
s.mulIndicator f = f
theorem Set.indicator_eq_self_of_superset {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {t : Set α} {f : αM} (h1 : s.indicator f = f) (h2 : s t) :
t.indicator f = f
theorem Set.mulIndicator_eq_self_of_superset {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {t : Set α} {f : αM} (h1 : s.mulIndicator f = f) (h2 : s t) :
t.mulIndicator f = f
@[simp]
theorem Set.indicator_apply_eq_zero {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {a : α} :
s.indicator f 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 : α} :
s.mulIndicator f 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} :
(s.indicator f = fun (x : α) => 0)
@[simp]
theorem Set.mulIndicator_eq_one {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
(s.mulIndicator f = fun (x : α) => 1)
@[simp]
theorem Set.indicator_eq_zero' {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} :
s.indicator f = 0
@[simp]
theorem Set.mulIndicator_eq_one' {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
s.mulIndicator f = 1
theorem Set.indicator_apply_ne_zero {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {a : α} :
s.indicator f a 0 a
theorem Set.mulIndicator_apply_ne_one {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} {a : α} :
s.mulIndicator f a 1 a
@[simp]
theorem Set.support_indicator {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} :
Function.support (s.indicator f) =
@[simp]
theorem Set.mulSupport_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
Function.mulSupport (s.mulIndicator f) =
theorem Set.mem_of_indicator_ne_zero {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} {a : α} (h : s.indicator f a 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 : s.mulIndicator f a 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 (s.indicator f) f s
theorem Set.eqOn_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
Set.EqOn (s.mulIndicator f) f s
theorem Set.support_indicator_subset {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} :
Function.support (s.indicator f) s
theorem Set.mulSupport_mulIndicator_subset {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
Function.mulSupport (s.mulIndicator f) s
@[simp]
theorem Set.indicator_support {α : Type u_1} {M : Type u_4} [Zero M] {f : αM} :
.indicator f = f
@[simp]
theorem Set.mulIndicator_mulSupport {α : Type u_1} {M : Type u_4} [One M] {f : αM} :
.mulIndicator f = f
@[simp]
theorem Set.indicator_range_comp {α : Type u_1} {M : Type u_4} [Zero M] {ι : Sort u_6} (f : ια) (g : αM) :
(Set.range f).indicator g f = g f
@[simp]
theorem Set.mulIndicator_range_comp {α : Type u_1} {M : Type u_4} [One M] {ι : Sort u_6} (f : ια) (g : αM) :
(Set.range f).mulIndicator g 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) :
s.indicator f = s.indicator g
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) :
s.mulIndicator f = s.mulIndicator g
@[simp]
theorem Set.indicator_univ {α : Type u_1} {M : Type u_4} [Zero M] (f : αM) :
Set.univ.indicator f = f
@[simp]
theorem Set.mulIndicator_univ {α : Type u_1} {M : Type u_4} [One M] (f : αM) :
Set.univ.mulIndicator f = f
@[simp]
theorem Set.indicator_empty {α : Type u_1} {M : Type u_4} [Zero M] (f : αM) :
.indicator f = fun (x : α) => 0
@[simp]
theorem Set.mulIndicator_empty {α : Type u_1} {M : Type u_4} [One M] (f : αM) :
.mulIndicator f = fun (x : α) => 1
theorem Set.indicator_empty' {α : Type u_1} {M : Type u_4} [Zero M] (f : αM) :
.indicator f = 0
theorem Set.mulIndicator_empty' {α : Type u_1} {M : Type u_4} [One M] (f : αM) :
.mulIndicator f = 1
@[simp]
theorem Set.indicator_zero {α : Type u_1} (M : Type u_4) [Zero M] (s : Set α) :
(s.indicator fun (x : α) => 0) = fun (x : α) => 0
@[simp]
theorem Set.mulIndicator_one {α : Type u_1} (M : Type u_4) [One M] (s : Set α) :
(s.mulIndicator fun (x : α) => 1) = fun (x : α) => 1
@[simp]
theorem Set.indicator_zero' {α : Type u_1} (M : Type u_4) [Zero M] {s : Set α} :
s.indicator 0 = 0
@[simp]
theorem Set.mulIndicator_one' {α : Type u_1} (M : Type u_4) [One M] {s : Set α} :
s.mulIndicator 1 = 1
theorem Set.indicator_indicator {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (t : Set α) (f : αM) :
s.indicator (t.indicator f) = (s t).indicator f
theorem Set.mulIndicator_mulIndicator {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (t : Set α) (f : αM) :
s.mulIndicator (t.mulIndicator f) = (s t).mulIndicator f
@[simp]
theorem Set.indicator_inter_support {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : αM) :
(s ).indicator f = s.indicator f
@[simp]
theorem Set.mulIndicator_inter_mulSupport {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (f : αM) :
(s ).mulIndicator f = s.mulIndicator f
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 (s.indicator f x) = s.piecewise (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 (s.mulIndicator f x) = s.piecewise (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 : β} :
(f ⁻¹' s).indicator (g f) x = s.indicator 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 : β} :
(f ⁻¹' s).mulIndicator (g f) x = s.mulIndicator 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 : α} :
(g '' s).indicator f (g x) = s.indicator (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 : α} :
(g '' s).mulIndicator f (g x) = s.mulIndicator (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) :
s.indicator (g f) = g s.indicator f
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) :
s.mulIndicator (g f) = g s.mulIndicator f
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 (s.indicator (fun (x : α) => c) x)) = s.indicator 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 (s.mulIndicator (fun (x : α) => c) x)) = s.mulIndicator fun (x : α) => f c
theorem Set.indicator_preimage {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : αM) (B : Set M) :
s.indicator f ⁻¹' B = s.ite (f ⁻¹' B) (0 ⁻¹' B)
theorem Set.mulIndicator_preimage {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (f : αM) (B : Set M) :
s.mulIndicator f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B)
theorem Set.indicator_zero_preimage {α : Type u_1} {M : Type u_4} [Zero M] {t : Set α} (s : Set M) :
t.indicator 0 ⁻¹' s {Set.univ, }
theorem Set.mulIndicator_one_preimage {α : Type u_1} {M : Type u_4} [One M] {t : Set α} (s : Set M) :
t.mulIndicator 1 ⁻¹' 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)] :
(U.indicator 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)] :
(U.mulIndicator 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) :
(U.indicator 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) :
(U.mulIndicator 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) :
U.indicator 1 ⁻¹' 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) :
s.indicator f ⁻¹' 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) :
s.mulIndicator f ⁻¹' 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 (s.indicator f) 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 Set.range (s.mulIndicator f) 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 (s.indicator f a) (s.indicator g a)
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 (s.mulIndicator f a) (s.mulIndicator g a)
theorem Set.indicator_union_add_inter_apply {α : Type u_1} {M : Type u_4} [] (f : αM) (s : Set α) (t : Set α) (a : α) :
(s t).indicator f a + (s t).indicator f a = s.indicator f a + t.indicator f a
theorem Set.mulIndicator_union_mul_inter_apply {α : Type u_1} {M : Type u_4} [] (f : αM) (s : Set α) (t : Set α) (a : α) :
(s t).mulIndicator f a * (s t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
theorem Set.indicator_union_add_inter {α : Type u_1} {M : Type u_4} [] (f : αM) (s : Set α) (t : Set α) :
(s t).indicator f + (s t).indicator f = s.indicator f + t.indicator f
theorem Set.mulIndicator_union_mul_inter {α : Type u_1} {M : Type u_4} [] (f : αM) (s : Set α) (t : Set α) :
(s t).mulIndicator f * (s t).mulIndicator f = s.mulIndicator f * t.mulIndicator f
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) :
(s t).indicator f a = s.indicator f a + t.indicator 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) :
(s t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator 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) :
(s t).indicator f = fun (a : α) => s.indicator f a + t.indicator f a
theorem Set.mulIndicator_union_of_disjoint {α : Type u_1} {M : Type u_4} [] {s : Set α} {t : Set α} (h : Disjoint s t) (f : αM) :
(s t).mulIndicator f = fun (a : α) => s.mulIndicator f a * t.mulIndicator f a
theorem Set.indicator_symmDiff {α : Type u_1} {M : Type u_4} [] (s : Set α) (t : Set α) (f : αM) :
(symmDiff s t).indicator f = (s \ t).indicator f + (t \ s).indicator f
theorem Set.mulIndicator_symmDiff {α : Type u_1} {M : Type u_4} [] (s : Set α) (t : Set α) (f : αM) :
(symmDiff s t).mulIndicator f = (s \ t).mulIndicator f * (t \ s).mulIndicator f
theorem Set.indicator_add {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (g : αM) :
(s.indicator fun (a : α) => f a + g a) = fun (a : α) => s.indicator f a + s.indicator g a
theorem Set.mulIndicator_mul {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (g : αM) :
(s.mulIndicator fun (a : α) => f a * g a) = fun (a : α) => s.mulIndicator f a * s.mulIndicator g a
theorem Set.indicator_add' {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (g : αM) :
s.indicator (f + g) = s.indicator f + s.indicator g
theorem Set.mulIndicator_mul' {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (g : αM) :
s.mulIndicator (f * g) = s.mulIndicator f * s.mulIndicator g
@[simp]
theorem Set.indicator_compl_add_self_apply {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (a : α) :
s.indicator f a + s.indicator f a = f a
@[simp]
theorem Set.mulIndicator_compl_mul_self_apply {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (a : α) :
s.mulIndicator f a * s.mulIndicator f a = f a
@[simp]
theorem Set.indicator_compl_add_self {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) :
s.indicator f + s.indicator f = f
@[simp]
theorem Set.mulIndicator_compl_mul_self {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) :
s.mulIndicator f * s.mulIndicator f = f
@[simp]
theorem Set.indicator_self_add_compl_apply {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (a : α) :
s.indicator f a + s.indicator f a = f a
@[simp]
theorem Set.mulIndicator_self_mul_compl_apply {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) (a : α) :
s.mulIndicator f a * s.mulIndicator f a = f a
@[simp]
theorem Set.indicator_self_add_compl {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) :
s.indicator f + s.indicator f = f
@[simp]
theorem Set.mulIndicator_self_mul_compl {α : Type u_1} {M : Type u_4} [] (s : Set α) (f : αM) :
s.mulIndicator f * s.mulIndicator f = f
theorem Set.indicator_add_eq_left {α : Type u_1} {M : Type u_4} [] {f : αM} {g : αM} (h : ) :
.indicator (f + g) = f
theorem Set.mulIndicator_mul_eq_left {α : Type u_1} {M : Type u_4} [] {f : αM} {g : αM} (h : ) :
.mulIndicator (f * g) = f
theorem Set.indicator_add_eq_right {α : Type u_1} {M : Type u_4} [] {f : αM} {g : αM} (h : ) :
.indicator (f + g) = g
theorem Set.mulIndicator_mul_eq_right {α : Type u_1} {M : Type u_4} [] {f : αM} {g : αM} (h : ) :
.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) :
s.indicator f + s.indicator g = s.piecewise f g
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) :
s.mulIndicator f * s.mulIndicator g = s.piecewise f g
noncomputable def Set.indicatorHom {α : Type u_6} (M : Type u_7) [] (s : Set α) :
(αM) →+ αM

Set.indicator as an addMonoidHom.

Equations
• = { toFun := s.indicator, map_zero' := , map_add' := }
Instances For
theorem Set.indicatorHom.proof_1 {α : Type u_1} (M : Type u_2) [] (s : Set α) :
(s.indicator 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
• = { toFun := s.mulIndicator, map_one' := , map_mul' := }
Instances For
theorem Set.indicator_neg' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
s.indicator (-f) = -s.indicator f
theorem Set.mulIndicator_inv' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
s.mulIndicator f⁻¹ = (s.mulIndicator f)⁻¹
theorem Set.indicator_neg {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
(s.indicator fun (a : α) => -f a) = fun (a : α) => -s.indicator f a
theorem Set.mulIndicator_inv {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
(s.mulIndicator fun (a : α) => (f a)⁻¹) = fun (a : α) => (s.mulIndicator f a)⁻¹
theorem Set.indicator_sub {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) (g : αG) :
(s.indicator fun (a : α) => f a - g a) = fun (a : α) => s.indicator f a - s.indicator g a
theorem Set.mulIndicator_div {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) (g : αG) :
(s.mulIndicator fun (a : α) => f a / g a) = fun (a : α) => s.mulIndicator f a / s.mulIndicator g a
theorem Set.indicator_sub' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) (g : αG) :
s.indicator (f - g) = s.indicator f - s.indicator g
theorem Set.mulIndicator_div' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) (g : αG) :
s.mulIndicator (f / g) = s.mulIndicator f / s.mulIndicator g
theorem Set.indicator_compl' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
s.indicator f = f + -s.indicator f
theorem Set.mulIndicator_compl {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
s.mulIndicator f = f * (s.mulIndicator f)⁻¹
theorem Set.indicator_compl {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
s.indicator f = f - s.indicator f
theorem Set.mulIndicator_compl' {α : Type u_1} {G : Type u_6} [] (s : Set α) (f : αG) :
s.mulIndicator f = f / s.mulIndicator f
theorem Set.indicator_diff' {α : Type u_1} {G : Type u_6} [] {s : Set α} {t : Set α} (h : s t) (f : αG) :
(t \ s).indicator f = t.indicator f + -s.indicator f
theorem Set.mulIndicator_diff {α : Type u_1} {G : Type u_6} [] {s : Set α} {t : Set α} (h : s t) (f : αG) :
(t \ s).mulIndicator f = t.mulIndicator f * (s.mulIndicator f)⁻¹
theorem Set.indicator_diff {α : Type u_1} {G : Type u_6} [] {s : Set α} {t : Set α} (h : s t) (f : αG) :
(t \ s).indicator f = t.indicator f - s.indicator f
theorem Set.mulIndicator_diff' {α : Type u_1} {G : Type u_6} [] {s : Set α} {t : Set α} (h : s t) (f : αG) :
(t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f
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 ((symmDiff s t).indicator f x) = g (s.indicator f x - t.indicator f x)
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 ((symmDiff s t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
theorem AddMonoidHom.map_indicator {α : Type u_1} {M : Type u_6} {N : Type u_7} [] [] (f : M →+ N) (s : Set α) (g : αM) (x : α) :
f (s.indicator g x) = s.indicator (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 (s.mulIndicator g x) = s.mulIndicator (f g) x