Documentation

Mathlib.Algebra.Group.Indicator

Indicator function #

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 Function.support f s
      @[simp]
      theorem Set.mulIndicator_eq_self {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
      s.mulIndicator f = f Function.mulSupport f s
      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) Disjoint (Function.support f) s
      @[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) Disjoint (Function.mulSupport f) s
      @[simp]
      theorem Set.indicator_eq_zero' {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : αM} :
      s.indicator f = 0 Disjoint (Function.support f) s
      @[simp]
      theorem Set.mulIndicator_eq_one' {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : αM} :
      s.mulIndicator f = 1 Disjoint (Function.mulSupport f) s
      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 s Function.support f
      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 s Function.mulSupport f
      @[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 : 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} :
      (Function.support f).indicator f = f
      @[simp]
      theorem Set.mulIndicator_mulSupport {α : Type u_1} {M : Type u_4} [One M] {f : αM} :
      (Function.mulSupport f).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 Function.support f).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 Function.mulSupport f).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 : Function.Injective g) {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 : Function.Injective g) {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} [AddZeroClass M] (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} [MulOneClass M] (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} [AddZeroClass M] (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} [MulOneClass M] (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} [AddZeroClass M] {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} [MulOneClass M] {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} [AddZeroClass M] {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} [MulOneClass M] {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} [AddZeroClass M] (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} [MulOneClass M] (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} [AddZeroClass M] (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} [MulOneClass M] (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} [AddZeroClass M] (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} [MulOneClass M] (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} [AddZeroClass M] (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} [MulOneClass M] (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} [AddZeroClass M] (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} [MulOneClass M] (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} [AddZeroClass M] (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} [MulOneClass M] (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} [AddZeroClass M] (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} [MulOneClass M] (s : Set α) (f : αM) :
      s.mulIndicator f * s.mulIndicator f = f
      theorem Set.indicator_add_eq_left {α : Type u_1} {M : Type u_4} [AddZeroClass M] {f : αM} {g : αM} (h : Disjoint (Function.support f) (Function.support g)) :
      (Function.support f).indicator (f + g) = f
      theorem Set.mulIndicator_mul_eq_left {α : Type u_1} {M : Type u_4} [MulOneClass M] {f : αM} {g : αM} (h : Disjoint (Function.mulSupport f) (Function.mulSupport g)) :
      (Function.mulSupport f).mulIndicator (f * g) = f
      theorem Set.indicator_add_eq_right {α : Type u_1} {M : Type u_4} [AddZeroClass M] {f : αM} {g : αM} (h : Disjoint (Function.support f) (Function.support g)) :
      (Function.support g).indicator (f + g) = g
      theorem Set.mulIndicator_mul_eq_right {α : Type u_1} {M : Type u_4} [MulOneClass M] {f : αM} {g : αM} (h : Disjoint (Function.mulSupport f) (Function.mulSupport g)) :
      (Function.mulSupport g).mulIndicator (f * g) = g
      theorem Set.indicator_add_compl_eq_piecewise {α : Type u_1} {M : Type u_4} [AddZeroClass M] {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} [MulOneClass M] {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) [AddZeroClass M] (s : Set α) :
      (αM) →+ αM

      Set.indicator as an addMonoidHom.

      Equations
      Instances For
        theorem Set.indicatorHom.proof_1 {α : Type u_1} (M : Type u_2) [AddZeroClass M] (s : Set α) :
        (s.indicator fun (x : α) => 0) = fun (x : α) => 0
        noncomputable def Set.mulIndicatorHom {α : Type u_6} (M : Type u_7) [MulOneClass M] (s : Set α) :
        (αM) →* αM

        Set.mulIndicator as a monoidHom.

        Equations
        Instances For
          theorem Set.indicator_neg' {α : Type u_1} {G : Type u_6} [AddGroup G] (s : Set α) (f : αG) :
          s.indicator (-f) = -s.indicator f
          theorem Set.mulIndicator_inv' {α : Type u_1} {G : Type u_6} [Group G] (s : Set α) (f : αG) :
          s.mulIndicator f⁻¹ = (s.mulIndicator f)⁻¹
          theorem Set.indicator_neg {α : Type u_1} {G : Type u_6} [AddGroup G] (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} [Group G] (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} [AddGroup G] (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} [Group G] (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} [AddGroup G] (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} [Group G] (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} [AddGroup G] (s : Set α) (f : αG) :
          s.indicator f = f + -s.indicator f
          theorem Set.mulIndicator_compl {α : Type u_1} {G : Type u_6} [Group G] (s : Set α) (f : αG) :
          s.mulIndicator f = f * (s.mulIndicator f)⁻¹
          theorem Set.indicator_compl {α : Type u_1} {G : Type u_6} [AddGroup G] (s : Set α) (f : αG) :
          s.indicator f = f - s.indicator f
          theorem Set.mulIndicator_compl' {α : Type u_1} {G : Type u_6} [Group G] (s : Set α) (f : αG) :
          s.mulIndicator f = f / s.mulIndicator f
          theorem Set.indicator_diff' {α : Type u_1} {G : Type u_6} [AddGroup G] {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} [Group G] {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} [AddGroup G] {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} [Group G] {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} [AddGroup G] {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} [Group G] {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} [AddZeroClass M] [AddZeroClass N] (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} [MulOneClass M] [MulOneClass N] (f : M →* N) (s : Set α) (g : αM) (x : α) :
          f (s.mulIndicator g x) = s.mulIndicator (f g) x