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.

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.

@[simp]

theorem Set.piecewise_eq_indicator {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} [DecidablePred fun x => x ∈ s] : Set.piecewise s f 0 = Set.indicator s 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] : Set.piecewise s f 1 = Set.mulIndicator s f

theorem Set.indicator_apply {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : α → M) (a : α) [Decidable (a ∈ s)] : Set.indicator s 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)] : Set.mulIndicator s 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) : Set.indicator s 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) : Set.mulIndicator s f a = 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) : Set.indicator s f a = 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) : Set.mulIndicator s f a = 1

theorem Set.indicator_eq_zero_or_self {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : α → M) (a : α) : Set.indicator s f a = 0 ∨ Set.indicator s 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 : α) : Set.mulIndicator s f a = 1 ∨ Set.mulIndicator s 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 : α} : Set.indicator s f a = f a ↔ ¬a ∈ s → f a = 0

@[simp]

theorem Set.mulIndicator_apply_eq_self {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} {a : α} : Set.mulIndicator s f a = f a ↔ ¬a ∈ s → f a = 1

@[simp]

theorem Set.indicator_eq_self {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} : Set.indicator s 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} : Set.mulIndicator s 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 : Set.indicator s f = f) (h2 : s ⊆ t) : Set.indicator t 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 : Set.mulIndicator s f = f) (h2 : s ⊆ t) : Set.mulIndicator t f = f

@[simp]

theorem Set.indicator_apply_eq_zero {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} {a : α} : Set.indicator s f a = 0 ↔ a ∈ s → f a = 0

@[simp]

theorem Set.mulIndicator_apply_eq_one {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} {a : α} : Set.mulIndicator s f a = 1 ↔ a ∈ s → f a = 1

@[simp]

theorem Set.indicator_eq_zero {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} : (Set.indicator s 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} : (Set.mulIndicator s 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} : Set.indicator s 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} : Set.mulIndicator s 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 : α} : Set.indicator s 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 : α} : Set.mulIndicator s 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} : Function.support (Set.indicator s f) = s ∩ Function.support f

@[simp]

theorem Set.mulSupport_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} : Function.mulSupport (Set.mulIndicator s f) = s ∩ Function.mulSupport f

theorem Set.mem_of_indicator_ne_zero {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} {a : α} (h : Set.indicator s 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 : Set.mulIndicator s 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 (Set.indicator s f) f s

theorem Set.eqOn_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} : Set.EqOn (Set.mulIndicator s f) f s

theorem Set.support_indicator_subset {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} : Function.support (Set.indicator s f) ⊆ s

theorem Set.mulSupport_mulIndicator_subset {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} : Function.mulSupport (Set.mulIndicator s f) ⊆ s

@[simp]

theorem Set.indicator_support {α : Type u_1} {M : Type u_4} [Zero M] {f : α → M} : Set.indicator (Function.support f) f = f

@[simp]

theorem Set.mulIndicator_mulSupport {α : Type u_1} {M : Type u_4} [One M] {f : α → M} : Set.mulIndicator (Function.mulSupport f) f = f

@[simp]

theorem Set.indicator_range_comp {α : Type u_1} {M : Type u_4} [Zero M] {ι : Sort u_6} (f : ι → α) (g : α → M) : Set.indicator (Set.range f) 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.mulIndicator (Set.range f) 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) : Set.indicator s f = Set.indicator s 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) : Set.mulIndicator s f = Set.mulIndicator s g

@[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) : Set.indicator ∅ f = fun x => 0

@[simp]

theorem Set.mulIndicator_empty {α : Type u_1} {M : Type u_4} [One M] (f : α → M) : Set.mulIndicator ∅ f = fun x => 1

theorem Set.indicator_empty' {α : Type u_1} {M : Type u_4} [Zero M] (f : α → M) : Set.indicator ∅ f = 0

theorem Set.mulIndicator_empty' {α : Type u_1} {M : Type u_4} [One M] (f : α → M) : Set.mulIndicator ∅ f = 1

@[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 α} : Set.indicator s 0 = 0

@[simp]

theorem Set.mulIndicator_one' {α : Type u_1} (M : Type u_4) [One M] {s : Set α} : Set.mulIndicator s 1 = 1

theorem Set.indicator_indicator {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (t : Set α) (f : α → M) : Set.indicator s (Set.indicator t f) = Set.indicator (s ∩ t) f

theorem Set.mulIndicator_mulIndicator {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (t : Set α) (f : α → M) : Set.mulIndicator s (Set.mulIndicator t f) = Set.mulIndicator (s ∩ t) f

@[simp]

theorem Set.indicator_inter_support {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : α → M) : Set.indicator (s ∩ Function.support f) f = Set.indicator s f

@[simp]

theorem Set.mulIndicator_inter_mulSupport {α : Type u_1} {M : Type u_4} [One M] (s : Set α) (f : α → M) : Set.mulIndicator (s ∩ Function.mulSupport f) f = Set.mulIndicator s 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 (Set.indicator s f x) = 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.mulIndicator s f x) = 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 : Function.Injective g) {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 : Function.Injective g) {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 : M → N} (hg : g 0 = 0) : Set.indicator s (g ∘ f) = g ∘ Set.indicator s 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 : M → N} (hg : g 1 = 1) : Set.mulIndicator s (g ∘ f) = g ∘ Set.mulIndicator s 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 : M → N) (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 : M → N) (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) : Set.indicator s f ⁻¹' 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) : Set.mulIndicator s f ⁻¹' 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) : Set.indicator t 0 ⁻¹' s ∈ {Set.univ, ∅}

theorem Set.mulIndicator_one_preimage {α : Type u_1} {M : Type u_4} [One M] {t : Set α} (s : Set M) : Set.mulIndicator t 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)] : (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) : Set.indicator U 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 : ¬0 ∈ t) : Set.indicator s 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 : ¬1 ∈ t) : Set.mulIndicator s 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 (Set.indicator s 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 (Set.mulIndicator s 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 : M → M → Prop} (h1 : r 0 0) (ha : a ∈ s → r (f a) (g a)) : r (Set.indicator s f a) (Set.indicator s g a)

theorem Set.mulIndicator_rel_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} {g : α → M} {a : α} {r : M → M → Prop} (h1 : r 1 1) (ha : a ∈ s → r (f a) (g a)) : r (Set.mulIndicator s f a) (Set.mulIndicator s 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 : α) : Set.indicator (s ∪ t) f a + Set.indicator (s ∩ t) f a = Set.indicator s f a + Set.indicator t 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 : α) : Set.mulIndicator (s ∪ t) f a * Set.mulIndicator (s ∩ t) f a = Set.mulIndicator s f a * Set.mulIndicator t f a

theorem Set.indicator_union_add_inter {α : Type u_1} {M : Type u_4} [AddZeroClass M] (f : α → M) (s : Set α) (t : Set α) : Set.indicator (s ∪ t) f + Set.indicator (s ∩ t) f = Set.indicator s f + Set.indicator t f

theorem Set.mulIndicator_union_mul_inter {α : Type u_1} {M : Type u_4} [MulOneClass M] (f : α → M) (s : Set α) (t : Set α) : Set.mulIndicator (s ∪ t) f * Set.mulIndicator (s ∩ t) f = Set.mulIndicator s f * Set.mulIndicator t f

theorem Set.indicator_union_of_not_mem_inter {α : Type u_1} {M : Type u_4} [AddZeroClass M] {s : Set α} {t : Set α} {a : α} (h : ¬a ∈ s ∩ t) (f : α → M) : Set.indicator (s ∪ t) f a = Set.indicator s f a + Set.indicator t 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 : ¬a ∈ s ∩ t) (f : α → M) : Set.mulIndicator (s ∪ t) f a = Set.mulIndicator s f a * Set.mulIndicator t 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) : Set.indicator (s ∪ t) f = fun a => Set.indicator s f a + Set.indicator t 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) : Set.mulIndicator (s ∪ t) f = fun a => Set.mulIndicator s f a * Set.mulIndicator t f a

theorem Set.indicator_symmDiff {α : Type u_1} {M : Type u_4} [AddZeroClass M] (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} [MulOneClass M] (s : Set α) (t : Set α) (f : α → M) : Set.mulIndicator (s ∆ t) f = Set.mulIndicator (s \ t) f * Set.mulIndicator (t \ s) f

theorem Set.indicator_add {α : Type u_1} {M : Type u_4} [AddZeroClass M] (s : Set α) (f : α → M) (g : α → M) : (Set.indicator s fun a => f a + g a) = fun a => Set.indicator s f a + Set.indicator s g a

theorem Set.mulIndicator_mul {α : Type u_1} {M : Type u_4} [MulOneClass M] (s : Set α) (f : α → M) (g : α → M) : (Set.mulIndicator s fun a => f a * g a) = fun a => Set.mulIndicator s f a * Set.mulIndicator s g a

theorem Set.indicator_add' {α : Type u_1} {M : Type u_4} [AddZeroClass M] (s : Set α) (f : α → M) (g : α → M) : Set.indicator s (f + g) = Set.indicator s f + Set.indicator s g

theorem Set.mulIndicator_mul' {α : Type u_1} {M : Type u_4} [MulOneClass M] (s : Set α) (f : α → M) (g : α → M) : Set.mulIndicator s (f * g) = Set.mulIndicator s f * Set.mulIndicator s g

@[simp]

theorem Set.indicator_compl_add_self_apply {α : Type u_1} {M : Type u_4} [AddZeroClass M] (s : Set α) (f : α → M) (a : α) : Set.indicator sᶜ f a + Set.indicator s 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 : α) : Set.mulIndicator sᶜ f a * Set.mulIndicator s f a = f a

@[simp]

theorem Set.indicator_compl_add_self {α : Type u_1} {M : Type u_4} [AddZeroClass M] (s : Set α) (f : α → M) : Set.indicator sᶜ f + Set.indicator s f = f

@[simp]

theorem Set.mulIndicator_compl_mul_self {α : Type u_1} {M : Type u_4} [MulOneClass M] (s : Set α) (f : α → M) : Set.mulIndicator sᶜ f * Set.mulIndicator s f = f

@[simp]

theorem Set.indicator_self_add_compl_apply {α : Type u_1} {M : Type u_4} [AddZeroClass M] (s : Set α) (f : α → M) (a : α) : Set.indicator s f a + Set.indicator sᶜ 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 : α) : Set.mulIndicator s f a * Set.mulIndicator sᶜ f a = f a

@[simp]

theorem Set.indicator_self_add_compl {α : Type u_1} {M : Type u_4} [AddZeroClass M] (s : Set α) (f : α → M) : Set.indicator s f + Set.indicator sᶜ f = f

@[simp]

theorem Set.mulIndicator_self_mul_compl {α : Type u_1} {M : Type u_4} [MulOneClass M] (s : Set α) (f : α → M) : Set.mulIndicator s f * Set.mulIndicator sᶜ 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)) : Set.indicator (Function.support f) (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)) : Set.mulIndicator (Function.mulSupport f) (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)) : Set.indicator (Function.support g) (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)) : Set.mulIndicator (Function.mulSupport g) (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) : Set.indicator s f + Set.indicator sᶜ g = Set.piecewise s 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) : Set.mulIndicator s f * Set.mulIndicator sᶜ g = Set.piecewise s f g

theorem Set.indicatorHom.proof_1 {α : Type u_1} (M : Type u_2) [AddZeroClass M] (s : Set α) : (Set.indicator s fun x => 0) = fun x => 0

noncomputable def Set.indicatorHom {α : Type u_6} (M : Type u_7) [AddZeroClass M] (s : Set α) : (α → M) →+ α → M

Set.indicator as an addMonoidHom.

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

Set.mulIndicator as a monoidHom.

theorem Set.indicator_smul_apply {α : Type u_1} {M : Type u_4} {A : Type u_6} [AddMonoid A] [Monoid M] [DistribMulAction M A] (s : Set α) (r : α → M) (f : α → A) (x : α) : Set.indicator s (fun x => r x • f x) x = r x • Set.indicator s f x

theorem Set.indicator_smul {α : Type u_1} {M : Type u_4} {A : Type u_6} [AddMonoid A] [Monoid M] [DistribMulAction M A] (s : Set α) (r : α → M) (f : α → A) : (Set.indicator s fun x => r x • f x) = fun x => r x • Set.indicator s f x

theorem Set.indicator_const_smul_apply {α : Type u_1} {M : Type u_4} {A : Type u_6} [AddMonoid A] [Monoid M] [DistribMulAction M A] (s : Set α) (r : M) (f : α → A) (x : α) : Set.indicator s (fun x => r • f x) x = r • Set.indicator s f x

theorem Set.indicator_const_smul {α : Type u_1} {M : Type u_4} {A : Type u_6} [AddMonoid A] [Monoid M] [DistribMulAction M A] (s : Set α) (r : M) (f : α → A) : (Set.indicator s fun x => r • f x) = fun x => r • Set.indicator s f x

theorem Set.indicator_smul_apply_left {α : Type u_1} {M : Type u_4} {A : Type u_6} [Zero A] [Zero M] [SMulWithZero M A] (s : Set α) (r : α → M) (f : α → A) (x : α) : Set.indicator s (fun x => r x • f x) x = Set.indicator s r x • f x

theorem Set.indicator_smul_left {α : Type u_1} {M : Type u_4} {A : Type u_6} [Zero A] [Zero M] [SMulWithZero M A] (s : Set α) (r : α → M) (f : α → A) : (Set.indicator s fun x => r x • f x) = fun x => Set.indicator s r x • f x

theorem Set.indicator_smul_const_apply {α : Type u_1} {M : Type u_4} {A : Type u_6} [Zero A] [Zero M] [SMulWithZero M A] (s : Set α) (r : α → M) (a : A) (x : α) : Set.indicator s (fun x => r x • a) x = Set.indicator s r x • a

theorem Set.indicator_smul_const {α : Type u_1} {M : Type u_4} {A : Type u_6} [Zero A] [Zero M] [SMulWithZero M A] (s : Set α) (r : α → M) (a : A) : (Set.indicator s fun x => r x • a) = fun x => Set.indicator s r x • a

theorem Set.indicator_neg' {α : Type u_1} {G : Type u_6} [AddGroup G] (s : Set α) (f : α → G) : Set.indicator s (-f) = -Set.indicator s f

theorem Set.mulIndicator_inv' {α : Type u_1} {G : Type u_6} [Group G] (s : Set α) (f : α → G) : Set.mulIndicator s f⁻¹ = (Set.mulIndicator s f)⁻¹

theorem Set.indicator_neg {α : Type u_1} {G : Type u_6} [AddGroup G] (s : Set α) (f : α → G) : (Set.indicator s fun a => -f a) = fun a => -Set.indicator s f a

theorem Set.mulIndicator_inv {α : Type u_1} {G : Type u_6} [Group G] (s : Set α) (f : α → G) : (Set.mulIndicator s fun a => (f a)⁻¹) = fun a => (Set.mulIndicator s f a)⁻¹

theorem Set.indicator_sub {α : Type u_1} {G : Type u_6} [AddGroup G] (s : Set α) (f : α → G) (g : α → G) : (Set.indicator s fun a => f a - g a) = fun a => Set.indicator s f a - Set.indicator s g a

theorem Set.mulIndicator_div {α : Type u_1} {G : Type u_6} [Group G] (s : Set α) (f : α → G) (g : α → G) : (Set.mulIndicator s fun a => f a / g a) = fun a => Set.mulIndicator s f a / Set.mulIndicator s g a

theorem Set.indicator_sub' {α : Type u_1} {G : Type u_6} [AddGroup G] (s : Set α) (f : α → G) (g : α → G) : Set.indicator s (f - g) = Set.indicator s f - Set.indicator s g

theorem Set.mulIndicator_div' {α : Type u_1} {G : Type u_6} [Group G] (s : Set α) (f : α → G) (g : α → G) : Set.mulIndicator s (f / g) = Set.mulIndicator s f / Set.mulIndicator s g

theorem Set.indicator_compl' {α : Type u_1} {G : Type u_6} [AddGroup G] (s : Set α) (f : α → G) : Set.indicator sᶜ f = f + -Set.indicator s f

theorem Set.mulIndicator_compl {α : Type u_1} {G : Type u_6} [Group G] (s : Set α) (f : α → G) : Set.mulIndicator sᶜ f = f * (Set.mulIndicator s f)⁻¹

theorem Set.indicator_compl {α : Type u_1} {G : Type u_6} [AddGroup G] (s : Set α) (f : α → G) : Set.indicator sᶜ f = f - Set.indicator s f

theorem Set.mulIndicator_compl' {α : Type u_1} {G : Type u_6} [Group G] (s : Set α) (f : α → G) : Set.mulIndicator sᶜ f = f / Set.mulIndicator s f

theorem Set.indicator_diff' {α : Type u_1} {G : Type u_6} [AddGroup G] {s : Set α} {t : Set α} (h : s ⊆ t) (f : α → G) : Set.indicator (t \ s) f = Set.indicator t f + -Set.indicator s f

theorem Set.mulIndicator_diff {α : Type u_1} {G : Type u_6} [Group G] {s : Set α} {t : Set α} (h : s ⊆ t) (f : α → G) : Set.mulIndicator (t \ s) f = Set.mulIndicator t f * (Set.mulIndicator s f)⁻¹

theorem Set.indicator_diff {α : Type u_1} {G : Type u_6} [AddGroup G] {s : Set α} {t : Set α} (h : s ⊆ t) (f : α → G) : Set.indicator (t \ s) f = Set.indicator t f - Set.indicator s f

theorem Set.mulIndicator_diff' {α : Type u_1} {G : Type u_6} [Group G] {s : Set α} {t : Set α} (h : s ⊆ t) (f : α → G) : Set.mulIndicator (t \ s) f = Set.mulIndicator t f / Set.mulIndicator s 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 (Set.indicator (s ∆ t) f x) = g (Set.indicator s f x - Set.indicator t 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 (Set.mulIndicator (s ∆ t) f x) = g (Set.mulIndicator s f x / Set.mulIndicator t f x)

theorem Set.abs_indicator_symmDiff {α : Type u_1} {G : Type u_6} [LinearOrderedAddCommGroup G] (s : Set α) (t : Set α) (f : α → G) (x : α) : |Set.indicator (s ∆ t) f x| = |Set.indicator s f x - Set.indicator t f x|

theorem Set.sum_indicator_subset_of_eq_zero {α : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [Zero N] (f : α → N) (g : α → N → M) {s : Finset α} {t : Finset α} (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} [CommMonoid M] [One N] (f : α → N) (g : α → N → M) {s : Finset α} {t : Finset α} (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} [AddCommMonoid M] (f : α → M) {s : Finset α} {t : Finset α} (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} [CommMonoid M] (f : α → M) {s : Finset α} {t : Finset α} (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} [AddCommMonoid M] (s : Finset ι) (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} [CommMonoid M] (s : Finset ι) (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} [AddCommMonoid M] (I : Finset ι) (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} [CommMonoid M] (I : Finset ι) (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} [AddCommMonoid M] (I : Finset ι) (s : ι → Set α) {f : α → M} : (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (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} [CommMonoid M] (I : Finset ι) (s : ι → Set α) {f : α → M} : (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (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} [AddCommMonoid M] (I : Finset ι) (s : ι → Set α) {f : α → M} (h : ∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (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} [CommMonoid M] (I : Finset ι) (s : ι → Set α) {f : α → M} (h : ∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (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} [MulZeroClass M] (s : Set α) (f : α → M) (g : α → M) : (Set.indicator s fun a => f a * g a) = fun a => Set.indicator s f a * Set.indicator s g a

theorem Set.indicator_mul_left {α : Type u_1} {M : Type u_4} [MulZeroClass M] {a : α} (s : Set α) (f : α → M) (g : α → M) : Set.indicator s (fun a => f a * g a) a = Set.indicator s f a * g a

theorem Set.indicator_mul_right {α : Type u_1} {M : Type u_4} [MulZeroClass M] {a : α} (s : Set α) (f : α → M) (g : α → M) : Set.indicator s (fun a => f a * g a) a = f a * Set.indicator s g a

theorem Set.inter_indicator_mul {α : Type u_1} {M : Type u_4} [MulZeroClass M] {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} [MulZeroOneClass M] {s : Set α} {t : Set α} : Set.indicator (s ∩ t) 1 = Set.indicator s 1 * Set.indicator t 1

theorem Set.indicator_prod_one {α : Type u_1} {β : Type u_2} {M : Type u_4} [MulZeroOneClass M] {s : Set α} {t : Set β} {x : α} {y : β} : Set.indicator (s ×ˢ t) 1 (x, y) = Set.indicator s 1 x * Set.indicator t 1 y

theorem Set.indicator_eq_zero_iff_not_mem {α : Type u_1} (M : Type u_4) [MulZeroOneClass M] [Nontrivial M] {U : Set α} {x : α} : Set.indicator U 1 x = 0 ↔ ¬x ∈ U

theorem Set.indicator_eq_one_iff_mem {α : Type u_1} (M : Type u_4) [MulZeroOneClass M] [Nontrivial M] {U : Set α} {x : α} : Set.indicator U 1 x = 1 ↔ x ∈ U

theorem Set.indicator_one_inj {α : Type u_1} (M : Type u_4) [MulZeroOneClass M] [Nontrivial M] {U : Set α} {V : Set α} (h : Set.indicator U 1 = Set.indicator V 1) : 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 ∈ s → f a ≤ y) (hg : ¬a ∈ s → 0 ≤ y) : Set.indicator s f a ≤ 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 ∈ s → f a ≤ y) (hg : ¬a ∈ s → 1 ≤ y) : Set.mulIndicator s f a ≤ 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 ∈ s → f a ≤ g a) (hg : ∀ (a : α), ¬a ∈ s → 0 ≤ g a) : Set.indicator s f ≤ 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 ∈ s → f a ≤ g a) (hg : ∀ (a : α), ¬a ∈ s → 1 ≤ g a) : Set.mulIndicator s f ≤ 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 ∈ s → y ≤ g a) (hf : ¬a ∈ s → y ≤ 0) : y ≤ Set.indicator s g a

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 ∈ s → y ≤ g a) (hf : ¬a ∈ s → y ≤ 1) : y ≤ Set.mulIndicator s g a

theorem Set.le_indicator {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} {g : α → M} [LE M] (hfg : ∀ (a : α), a ∈ s → f a ≤ g a) (hf : ∀ (a : α), ¬a ∈ s → f a ≤ 0) : f ≤ Set.indicator s g

theorem Set.le_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} {g : α → M} [LE M] (hfg : ∀ (a : α), a ∈ s → f a ≤ g a) (hf : ∀ (a : α), ¬a ∈ s → f a ≤ 1) : f ≤ Set.mulIndicator s g

theorem Set.indicator_apply_nonneg {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} {a : α} [Preorder M] (h : a ∈ s → 0 ≤ f a) : 0 ≤ Set.indicator s f a

theorem Set.one_le_mulIndicator_apply {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} {a : α} [Preorder M] (h : a ∈ s → 1 ≤ f a) : 1 ≤ Set.mulIndicator s f a

theorem Set.indicator_nonneg {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} [Preorder M] (h : ∀ (a : α), a ∈ s → 0 ≤ f a) (a : α) : 0 ≤ Set.indicator s f a

theorem Set.one_le_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} [Preorder M] (h : ∀ (a : α), a ∈ s → 1 ≤ f a) (a : α) : 1 ≤ Set.mulIndicator s f a

theorem Set.indicator_apply_nonpos {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} {a : α} [Preorder M] (h : a ∈ s → f a ≤ 0) : Set.indicator s f a ≤ 0

theorem Set.mulIndicator_apply_le_one {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} {a : α} [Preorder M] (h : a ∈ s → f a ≤ 1) : Set.mulIndicator s f a ≤ 1

theorem Set.indicator_nonpos {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} [Preorder M] (h : ∀ (a : α), a ∈ s → f a ≤ 0) (a : α) : Set.indicator s f a ≤ 0

theorem Set.mulIndicator_le_one {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} [Preorder M] (h : ∀ (a : α), a ∈ s → f a ≤ 1) (a : α) : Set.mulIndicator s f a ≤ 1

theorem Set.indicator_le_indicator {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} {g : α → M} {a : α} [Preorder M] (h : f a ≤ g a) : Set.indicator s f a ≤ Set.indicator s g a

theorem Set.mulIndicator_le_mulIndicator {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} {g : α → M} {a : α} [Preorder M] (h : f a ≤ g a) : Set.mulIndicator s f a ≤ Set.mulIndicator s g a

theorem Set.indicator_le_indicator_of_subset {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {t : Set α} {f : α → M} [Preorder M] (h : s ⊆ t) (hf : ∀ (a : α), 0 ≤ f a) (a : α) : Set.indicator s f a ≤ Set.indicator t f a

theorem Set.mulIndicator_le_mulIndicator_of_subset {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {t : Set α} {f : α → M} [Preorder M] (h : s ⊆ t) (hf : ∀ (a : α), 1 ≤ f a) (a : α) : Set.mulIndicator s f a ≤ Set.mulIndicator t f a

theorem Set.indicator_le_self' {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α → M} [Preorder M] (hf : ∀ (x : α), ¬x ∈ s → 0 ≤ f x) : Set.indicator s f ≤ f

theorem Set.mulIndicator_le_self' {α : Type u_1} {M : Type u_4} [One M] {s : Set α} {f : α → M} [Preorder M] (hf : ∀ (x : α), ¬x ∈ s → 1 ≤ f x) : Set.mulIndicator s f ≤ f

theorem Set.indicator_iUnion_apply {α : Type u_1} {ι : Sort u_6} {M : Type u_7} [CompleteLattice M] [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} [CompleteLattice M] [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} [Nonempty ι] [CompleteLattice M] [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} [Nonempty ι] [CompleteLattice M] [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} [CanonicallyOrderedAddMonoid M] (s : Set α) (f : α → M) : Set.indicator s f ≤ f

theorem Set.mulIndicator_le_self {α : Type u_1} {M : Type u_4} [CanonicallyOrderedMonoid M] (s : Set α) (f : α → M) : Set.mulIndicator s f ≤ f

theorem Set.indicator_apply_le {α : Type u_1} {M : Type u_4} [CanonicallyOrderedAddMonoid M] {a : α} {s : Set α} {f : α → M} {g : α → M} (hfg : a ∈ s → f a ≤ g a) : Set.indicator s f a ≤ g a

theorem Set.mulIndicator_apply_le {α : Type u_1} {M : Type u_4} [CanonicallyOrderedMonoid M] {a : α} {s : Set α} {f : α → M} {g : α → M} (hfg : a ∈ s → f a ≤ g a) : Set.mulIndicator s f a ≤ g a

theorem Set.indicator_le {α : Type u_1} {M : Type u_4} [CanonicallyOrderedAddMonoid M] {s : Set α} {f : α → M} {g : α → M} (hfg : ∀ (a : α), a ∈ s → f a ≤ g a) : Set.indicator s f ≤ g

theorem Set.mulIndicator_le {α : Type u_1} {M : Type u_4} [CanonicallyOrderedMonoid M] {s : Set α} {f : α → M} {g : α → M} (hfg : ∀ (a : α), a ∈ s → f a ≤ g a) : Set.mulIndicator s f ≤ g

theorem Set.indicator_le_indicator_nonneg {α : Type u_1} {β : Type u_6} [LinearOrder β] [Zero β] (s : Set α) (f : α → β) : Set.indicator s f ≤ Set.indicator {x | 0 ≤ f x} f

theorem Set.indicator_nonpos_le_indicator {α : Type u_1} {β : Type u_6} [LinearOrder β] [Zero β] (s : Set α) (f : α → β) : Set.indicator {x | f x ≤ 0} f ≤ Set.indicator s f

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 (Set.indicator s g x) = Set.indicator s (↑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 (Set.mulIndicator s g x) = Set.mulIndicator s (↑f ∘ g) x