Indicator function

This file defines the indicator function of a set. More lemmas can be found in Mathlib/Algebra/Group/Indicator.lean.

Main declarations

• 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.mulIndicator {α : Type u_1} {M : Type u_3} [One M] (s : Set α) (f : α → M) (x : α) : M

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

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

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

@[simp]

theorem Set.piecewise_eq_mulIndicator {α : Type u_1} {M : Type u_3} [One M] {s : Set α} {f : α → M} [DecidablePred fun (x : α) => x ∈ s] : s.piecewise f 1 = s.mulIndicator f

@[simp]

theorem Set.piecewise_eq_indicator {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {f : α → M} [DecidablePred fun (x : α) => x ∈ s] : s.piecewise f 0 = s.indicator f

theorem Set.mulIndicator_apply {α : Type u_1} {M : Type u_3} [One M] (s : Set α) (f : α → M) (a : α) [Decidable (a ∈ s)] : s.mulIndicator f a = if a ∈ s then f a else 1

theorem Set.indicator_apply {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) (a : α) [Decidable (a ∈ s)] : s.indicator f a = if a ∈ s then f a else 0

@[simp]

theorem Set.mulIndicator_of_mem {α : Type u_1} {M : Type u_3} [One M] {s : Set α} {a : α} (h : a ∈ s) (f : α → M) : s.mulIndicator f a = f a

@[simp]

theorem Set.indicator_of_mem {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {a : α} (h : a ∈ s) (f : α → M) : s.indicator f a = f a

@[simp]

theorem Set.mulIndicator_of_notMem {α : Type u_1} {M : Type u_3} [One M] {s : Set α} {a : α} (h : a ∉ s) (f : α → M) : s.mulIndicator f a = 1

@[simp]

theorem Set.indicator_of_notMem {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {a : α} (h : a ∉ s) (f : α → M) : s.indicator f a = 0

@[deprecated Set.indicator_of_notMem (since := "2025-05-23")]

theorem Set.indicator_of_not_mem {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {a : α} (h : a ∉ s) (f : α → M) : s.indicator f a = 0

Alias of Set.indicator_of_notMem.

@[deprecated Set.mulIndicator_of_notMem (since := "2025-05-23")]

theorem Set.mulIndicator_of_not_mem {α : Type u_1} {M : Type u_3} [One M] {s : Set α} {a : α} (h : a ∉ s) (f : α → M) : s.mulIndicator f a = 1

Alias of Set.mulIndicator_of_notMem.

theorem Set.mulIndicator_eq_one_or_self {α : Type u_1} {M : Type u_3} [One M] (s : Set α) (f : α → M) (a : α) : s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

theorem Set.indicator_eq_zero_or_self {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) (a : α) : s.indicator f a = 0 ∨ s.indicator f a = f a

@[simp]

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

@[simp]

theorem Set.indicator_apply_eq_self {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {f : α → M} {a : α} : s.indicator f a = f a ↔ a ∉ s → f a = 0

@[simp]

theorem Set.mulIndicator_eq_self {α : Type u_1} {M : Type u_3} [One M] {s : Set α} {f : α → M} : s.mulIndicator f = f ↔ Function.mulSupport f ⊆ s

@[simp]

theorem Set.indicator_eq_self {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {f : α → M} : s.indicator f = f ↔ Function.support f ⊆ s

theorem Set.mulIndicator_eq_self_of_superset {α : Type u_1} {M : Type u_3} [One M] {s t : Set α} {f : α → M} (h1 : s.mulIndicator f = f) (h2 : s ⊆ t) : t.mulIndicator f = f

theorem Set.indicator_eq_self_of_superset {α : Type u_1} {M : Type u_3} [Zero M] {s t : Set α} {f : α → M} (h1 : s.indicator f = f) (h2 : s ⊆ t) : t.indicator f = f

@[simp]

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

@[simp]

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

@[simp]

theorem Set.mulIndicator_eq_one {α : Type u_1} {M : Type u_3} [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_3} [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_3} [One M] {s : Set α} {f : α → M} : s.mulIndicator f = 1 ↔ Disjoint (Function.mulSupport f) s

@[simp]

theorem Set.indicator_eq_zero' {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {f : α → M} : s.indicator f = 0 ↔ Disjoint (Function.support f) s

theorem Set.mulIndicator_apply_ne_one {α : Type u_1} {M : Type u_3} [One M] {s : Set α} {f : α → M} {a : α} : s.mulIndicator f a ≠ 1 ↔ a ∈ s ∩ Function.mulSupport f

theorem Set.indicator_apply_ne_zero {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {f : α → M} {a : α} : s.indicator f a ≠ 0 ↔ a ∈ s ∩ Function.support f

@[simp]

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

@[simp]

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

theorem Set.mem_of_mulIndicator_ne_one {α : Type u_1} {M : Type u_3} [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.mem_of_indicator_ne_zero {α : Type u_1} {M : Type u_3} [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.eqOn_mulIndicator {α : Type u_1} {M : Type u_3} [One M] {s : Set α} {f : α → M} : EqOn (s.mulIndicator f) f s

See Set.eqOn_mulIndicator' for the version with sᶜ.

theorem Set.eqOn_indicator {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {f : α → M} : EqOn (s.indicator f) f s

See Set.eqOn_indicator' for the version with sᶜ.

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

See Set.eqOn_mulIndicator for the version with s.

theorem Set.eqOn_indicator' {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {f : α → M} : EqOn (s.indicator f) 0 sᶜ

See Set.eqOn_indicator for the version with s.

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Set.mulIndicator_range_comp {α : Type u_1} {M : Type u_3} [One M] {ι : Sort u_5} (f : ι → α) (g : α → M) : (range f).mulIndicator g ∘ f = g ∘ f

@[simp]

theorem Set.indicator_range_comp {α : Type u_1} {M : Type u_3} [Zero M] {ι : Sort u_5} (f : ι → α) (g : α → M) : (range f).indicator g ∘ f = g ∘ f

theorem Set.mulIndicator_congr {α : Type u_1} {M : Type u_3} [One M] {s : Set α} {f g : α → M} (h : EqOn f g s) : s.mulIndicator f = s.mulIndicator g

theorem Set.indicator_congr {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {f g : α → M} (h : EqOn f g s) : s.indicator f = s.indicator g

theorem Set.mulIndicator_eq_mulIndicator {α : Type u_1} {β : Type u_2} {M : Type u_3} [One M] {s : Set α} {f : α → M} {a : α} {t : Set β} {g : β → M} {b : β} (h1 : a ∈ s ↔ b ∈ t) (h2 : f a = g b) : s.mulIndicator f a = t.mulIndicator g b

theorem Set.indicator_eq_indicator {α : Type u_1} {β : Type u_2} {M : Type u_3} [Zero M] {s : Set α} {f : α → M} {a : α} {t : Set β} {g : β → M} {b : β} (h1 : a ∈ s ↔ b ∈ t) (h2 : f a = g b) : s.indicator f a = t.indicator g b

theorem Set.mulIndicator_const_eq_mulIndicator_const {α : Type u_1} {β : Type u_2} {M : Type u_3} [One M] {s : Set α} {a : α} {t : Set β} {b : β} {c : M} (h : a ∈ s ↔ b ∈ t) : s.mulIndicator (fun (x : α) => c) a = t.mulIndicator (fun (x : β) => c) b

theorem Set.indicator_const_eq_indicator_const {α : Type u_1} {β : Type u_2} {M : Type u_3} [Zero M] {s : Set α} {a : α} {t : Set β} {b : β} {c : M} (h : a ∈ s ↔ b ∈ t) : s.indicator (fun (x : α) => c) a = t.indicator (fun (x : β) => c) b

@[simp]

theorem Set.mulIndicator_univ {α : Type u_1} {M : Type u_3} [One M] (f : α → M) : univ.mulIndicator f = f

@[simp]

theorem Set.indicator_univ {α : Type u_1} {M : Type u_3} [Zero M] (f : α → M) : univ.indicator f = f

@[simp]

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

@[simp]

theorem Set.indicator_empty {α : Type u_1} {M : Type u_3} [Zero M] (f : α → M) : ∅.indicator f = fun (x : α) => 0

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

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

@[simp]

theorem Set.mulIndicator_one {α : Type u_1} (M : Type u_3) [One M] (s : Set α) : (s.mulIndicator fun (x : α) => 1) = fun (x : α) => 1

@[simp]

theorem Set.indicator_zero {α : Type u_1} (M : Type u_3) [Zero M] (s : Set α) : (s.indicator fun (x : α) => 0) = fun (x : α) => 0

@[simp]

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

@[simp]

theorem Set.indicator_zero' {α : Type u_1} (M : Type u_3) [Zero M] {s : Set α} : s.indicator 0 = 0

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

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

@[simp]

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

@[simp]

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

theorem Set.comp_mulIndicator {α : Type u_1} {β : Type u_2} {M : Type u_3} [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.comp_indicator {α : Type u_1} {β : Type u_2} {M : Type u_3} [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.mulIndicator_comp_right {α : Type u_1} {β : Type u_2} {M : Type u_3} [One M] {s : Set α} (f : β → α) {g : α → M} {x : β} : (f ⁻¹' s).mulIndicator (g ∘ f) x = s.mulIndicator g (f x)

theorem Set.indicator_comp_right {α : Type u_1} {β : Type u_2} {M : Type u_3} [Zero M] {s : Set α} (f : β → α) {g : α → M} {x : β} : (f ⁻¹' s).indicator (g ∘ f) x = s.indicator g (f x)

theorem Set.mulIndicator_image {α : Type u_1} {β : Type u_2} {M : Type u_3} [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_image {α : Type u_1} {β : Type u_2} {M : Type u_3} [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_comp_of_one {α : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] {s : Set α} {f : α → M} {g : M → N} (hg : g 1 = 1) : s.mulIndicator (g ∘ f) = g ∘ s.mulIndicator f

theorem Set.indicator_comp_of_zero {α : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {s : Set α} {f : α → M} {g : M → N} (hg : g 0 = 0) : s.indicator (g ∘ f) = g ∘ s.indicator f

theorem Set.comp_mulIndicator_const {α : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] {s : Set α} (c : M) (f : M → N) (hf : f 1 = 1) : (fun (x : α) => f (s.mulIndicator (fun (x : α) => c) x)) = s.mulIndicator fun (x : α) => f c

theorem Set.comp_indicator_const {α : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {s : Set α} (c : M) (f : M → N) (hf : f 0 = 0) : (fun (x : α) => f (s.indicator (fun (x : α) => c) x)) = s.indicator fun (x : α) => f c

theorem Set.mulIndicator_preimage {α : Type u_1} {M : Type u_3} [One M] (s : Set α) (f : α → M) (B : Set M) : s.mulIndicator f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B)

theorem Set.indicator_preimage {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) (B : Set M) : s.indicator f ⁻¹' B = s.ite (f ⁻¹' B) (0 ⁻¹' B)

theorem Set.mulIndicator_one_preimage {α : Type u_1} {M : Type u_3} [One M] {t : Set α} (s : Set M) : t.mulIndicator 1 ⁻¹' s ∈ {univ, ∅}

theorem Set.indicator_zero_preimage {α : Type u_1} {M : Type u_3} [Zero M] {t : Set α} (s : Set M) : t.indicator 0 ⁻¹' s ∈ {univ, ∅}

theorem Set.mulIndicator_const_preimage_eq_union {α : Type u_1} {M : Type u_3} [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_eq_union {α : Type u_1} {M : Type u_3} [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 {α : Type u_1} {M : Type u_3} [One M] (U : Set α) (s : Set M) (a : M) : (U.mulIndicator fun (x : α) => a) ⁻¹' s ∈ {univ, U, Uᶜ, ∅}

theorem Set.indicator_const_preimage {α : Type u_1} {M : Type u_3} [Zero M] (U : Set α) (s : Set M) (a : M) : (U.indicator fun (x : α) => a) ⁻¹' s ∈ {univ, U, Uᶜ, ∅}

theorem Set.mulIndicator_preimage_of_notMem {α : Type u_1} {M : Type u_3} [One M] (s : Set α) (f : α → M) {t : Set M} (ht : 1 ∉ t) : s.mulIndicator f ⁻¹' t = f ⁻¹' t ∩ s

theorem Set.indicator_preimage_of_notMem {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) {t : Set M} (ht : 0 ∉ t) : s.indicator f ⁻¹' t = f ⁻¹' t ∩ s

@[deprecated Set.indicator_preimage_of_notMem (since := "2025-05-23")]

theorem Set.indicator_preimage_of_not_mem {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) {t : Set M} (ht : 0 ∉ t) : s.indicator f ⁻¹' t = f ⁻¹' t ∩ s

Alias of Set.indicator_preimage_of_notMem.

@[deprecated Set.mulIndicator_preimage_of_notMem (since := "2025-05-23")]

theorem Set.mulIndicator_preimage_of_not_mem {α : Type u_1} {M : Type u_3} [One M] (s : Set α) (f : α → M) {t : Set M} (ht : 1 ∉ t) : s.mulIndicator f ⁻¹' t = f ⁻¹' t ∩ s

Alias of Set.mulIndicator_preimage_of_notMem.

theorem Set.mem_range_mulIndicator {α : Type u_1} {M : Type u_3} [One M] {r : M} {s : Set α} {f : α → M} : r ∈ range (s.mulIndicator f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s

theorem Set.mem_range_indicator {α : Type u_1} {M : Type u_3} [Zero M] {r : M} {s : Set α} {f : α → M} : r ∈ range (s.indicator f) ↔ r = 0 ∧ s ≠ univ ∨ r ∈ f '' s

theorem Set.mulIndicator_rel_mulIndicator {α : Type u_1} {M : Type u_3} [One M] {s : Set α} {f g : α → M} {a : α} {r : M → M → Prop} (h1 : r 1 1) (ha : a ∈ s → r (f a) (g a)) : r (s.mulIndicator f a) (s.mulIndicator g a)

theorem Set.indicator_rel_indicator {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {f g : α → M} {a : α} {r : M → M → Prop} (h1 : r 0 0) (ha : a ∈ s → r (f a) (g a)) : r (s.indicator f a) (s.indicator g a)

theorem Set.indicator_one_preimage {α : Type u_1} {M : Type u_3} [One M] [Zero M] (U : Set α) (s : Set M) : U.indicator 1 ⁻¹' s ∈ {univ, U, Uᶜ, ∅}