doc-next-gen

Mathlib.Algebra.Group.Indicator

Module docstring

{"# 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 "}

Set.mulIndicator definition
(s : Set α) (f : α → M) (x : α) : M
Full source 
/-- `Set.mulIndicator s f a` is `f a` if `a ∈ s`, `1` otherwise. -/
@[to_additive "`Set.indicator s f a` is `f a` if `a ∈ s`, `0` otherwise."]
noncomputable def mulIndicator (s : Set α) (f : α → M) (x : α) : M :=
  haveI := Classical.decPred (· ∈ s)
  if x ∈ s then f x else 1
Multiplicative indicator function
Informal description
For a set \( s \subseteq \alpha \) and a function \( f : \alpha \to M \), the multiplicative indicator function \( \text{mulIndicator} \, s \, f \) is defined as: \[ \text{mulIndicator} \, s \, f \, x = \begin{cases} f(x) & \text{if } x \in s, \\ 1 & \text{otherwise.} \end{cases} \] Here, \( M \) is a type with a multiplicative identity \( 1 \).
Set.piecewise_eq_mulIndicator theorem
[DecidablePred (· ∈ s)] : s.piecewise f 1 = s.mulIndicator f
Full source 
@[to_additive (attr := simp)]
theorem piecewise_eq_mulIndicator [DecidablePred (· ∈ s)] : s.piecewise f 1 = s.mulIndicator f :=
  funext fun _ => @if_congr _ _ _ _ (id _) _ _ _ _ Iff.rfl rfl rfl
Equality of Piecewise Function and Multiplicative Indicator Function
Informal description
For any set $s \subseteq \alpha$ with decidable membership and any function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the piecewise function defined by $f$ on $s$ and $1$ elsewhere is equal to the multiplicative indicator function of $s$ applied to $f$. That is: \[ s.\text{piecewise}\ f\ 1 = \text{mulIndicator}_s f \]
Set.mulIndicator_apply theorem
(s : Set α) (f : α → M) (a : α) [Decidable (a ∈ s)] : mulIndicator s f a = if a ∈ s then f a else 1
Full source 
@[to_additive]
theorem mulIndicator_apply (s : Set α) (f : α → M) (a : α) [Decidable (a ∈ s)] :
    mulIndicator s f a = if a ∈ s then f a else 1 := by
  unfold mulIndicator
  congr
Definition of Multiplicative Indicator Function
Informal description
For any set $s \subseteq \alpha$, function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), and element $a \in \alpha$, the multiplicative indicator function satisfies: \[ \text{mulIndicator}_s f (a) = \begin{cases} f(a) & \text{if } a \in s, \\ 1 & \text{otherwise.} \end{cases} \]
Set.mulIndicator_of_mem theorem
(h : a ∈ s) (f : α → M) : mulIndicator s f a = f a
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_of_mem (h : a ∈ s) (f : α → M) : mulIndicator s f a = f a :=
  if_pos h
Multiplicative Indicator Function Equals Original Function on Set
Informal description
For any set $s \subseteq \alpha$, function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), and element $a \in s$, the multiplicative indicator function satisfies $\text{mulIndicator}_s f (a) = f(a)$.
Set.mulIndicator_of_not_mem theorem
(h : a ∉ s) (f : α → M) : mulIndicator s f a = 1
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_of_not_mem (h : a ∉ s) (f : α → M) : mulIndicator s f a = 1 :=
  if_neg h
Multiplicative Indicator Function Equals One Outside Set
Informal description
For a set $s \subseteq \alpha$, a function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), and an element $a \in \alpha$ such that $a \notin s$, the multiplicative indicator function satisfies: \[ \text{mulIndicator}_s f (a) = 1. \]
Set.mulIndicator_eq_one_or_self theorem
(s : Set α) (f : α → M) (a : α) : mulIndicator s f a = 1 ∨ mulIndicator s f a = f a
Full source 
@[to_additive]
theorem mulIndicator_eq_one_or_self (s : Set α) (f : α → M) (a : α) :
    mulIndicatormulIndicator s f a = 1 ∨ mulIndicator s f a = f a := by
  by_cases h : a ∈ s
  · exact Or.inr (mulIndicator_of_mem h f)
  · exact Or.inl (mulIndicator_of_not_mem h f)
Multiplicative Indicator Function Takes Value One or Original Function Value
Informal description
For any set $s \subseteq \alpha$, function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), and element $a \in \alpha$, the multiplicative indicator function satisfies either $\text{mulIndicator}_s f (a) = 1$ or $\text{mulIndicator}_s f (a) = f(a)$.
Set.mulIndicator_apply_eq_self theorem
: s.mulIndicator f a = f a ↔ a ∉ s → f a = 1
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_apply_eq_self : s.mulIndicator f a = f a ↔ a ∉ s → f a = 1 :=
  letI := Classical.dec (a ∈ s)
  ite_eq_left_iff.trans (by rw [@eq_comm _ (f a)])
Characterization of Multiplicative Indicator Function Equality: $\text{mulIndicator}_s f (a) = f(a) \iff (a \notin s \to f(a) = 1)$
Informal description
For a set $s \subseteq \alpha$, a function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), and an element $a \in \alpha$, the multiplicative indicator function satisfies: \[ \text{mulIndicator}_s f (a) = f(a) \quad \text{if and only if} \quad (a \notin s \implies f(a) = 1). \]
Set.mulIndicator_eq_self theorem
: s.mulIndicator f = f ↔ mulSupport f ⊆ s
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_eq_self : s.mulIndicator f = f ↔ mulSupport f ⊆ s := by
  simp only [funext_iff, subset_def, mem_mulSupport, mulIndicator_apply_eq_self, not_imp_comm]
Characterization of Multiplicative Indicator Function Equality: $\text{mulIndicator}_s f = f \iff \text{mulSupport}(f) \subseteq s$
Informal description
For a set $s \subseteq \alpha$ and a function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative indicator function $\text{mulIndicator}_s f$ equals $f$ if and only if the multiplicative support of $f$ is contained in $s$. In other words: \[ \text{mulIndicator}_s f = f \iff \{x \in \alpha \mid f(x) \neq 1\} \subseteq s. \]
Set.mulIndicator_eq_self_of_superset theorem
(h1 : s.mulIndicator f = f) (h2 : s ⊆ t) : t.mulIndicator f = f
Full source 
@[to_additive]
theorem mulIndicator_eq_self_of_superset (h1 : s.mulIndicator f = f) (h2 : s ⊆ t) :
    t.mulIndicator f = f := by
  rw [mulIndicator_eq_self] at h1 ⊢
  exact Subset.trans h1 h2
Multiplicative Indicator Function Equality under Superset Condition
Informal description
For any sets \( s \subseteq t \subseteq \alpha \) and any function \( f : \alpha \to M \) (where \( M \) has a multiplicative identity \( 1 \)), if the multiplicative indicator function of \( f \) on \( s \) equals \( f \), then the multiplicative indicator function of \( f \) on \( t \) also equals \( f \). In other words: \[ \text{mulIndicator}_s f = f \text{ and } s \subseteq t \implies \text{mulIndicator}_t f = f. \]
Set.mulIndicator_apply_eq_one theorem
: mulIndicator s f a = 1 ↔ a ∈ s → f a = 1
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_apply_eq_one : mulIndicatormulIndicator s f a = 1 ↔ a ∈ s → f a = 1 :=
  letI := Classical.dec (a ∈ s)
  ite_eq_right_iff
Characterization of Multiplicative Indicator Value: $\text{mulIndicator}_s f (a) = 1 \iff (a \in s \to f(a) = 1)$
Informal description
For a set $s \subseteq \alpha$, a function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), and an element $a \in \alpha$, the multiplicative indicator function satisfies: \[ \text{mulIndicator}_s f (a) = 1 \iff (a \in s \implies f(a) = 1). \]
Set.mulIndicator_eq_one theorem
: (mulIndicator s f = fun _ => 1) ↔ Disjoint (mulSupport f) s
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_eq_one : (mulIndicator s f = fun _ => 1) ↔ Disjoint (mulSupport f) s := by
  simp only [funext_iff, mulIndicator_apply_eq_one, Set.disjoint_left, mem_mulSupport,
    not_imp_not]
Characterization of Constant One Multiplicative Indicator via Disjoint Support
Informal description
For a set $s \subseteq \alpha$ and a function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative indicator function $\text{mulIndicator}_s f$ is identically equal to the constant function $1$ if and only if the multiplicative support of $f$ is disjoint from $s$. That is: \[ \text{mulIndicator}_s f = \mathbf{1} \iff \text{mulSupport}(f) \cap s = \emptyset, \] where $\mathbf{1}$ denotes the constant function $x \mapsto 1$ and $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$.
Set.mulIndicator_eq_one' theorem
: mulIndicator s f = 1 ↔ Disjoint (mulSupport f) s
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_eq_one' : mulIndicatormulIndicator s f = 1 ↔ Disjoint (mulSupport f) s :=
  mulIndicator_eq_one
Multiplicative Indicator Equals One if and only if Support Disjoint from Set
Informal description
For a set $s \subseteq \alpha$ and a function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative indicator function $\text{mulIndicator}_s f$ is identically equal to the constant function $1$ if and only if the multiplicative support of $f$ is disjoint from $s$. That is: \[ \text{mulIndicator}_s f = \mathbf{1} \iff \text{mulSupport}(f) \cap s = \emptyset, \] where $\mathbf{1}$ denotes the constant function $x \mapsto 1$ and $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$.
Set.mulIndicator_apply_ne_one theorem
{a : α} : s.mulIndicator f a ≠ 1 ↔ a ∈ s ∩ mulSupport f
Full source 
@[to_additive]
theorem mulIndicator_apply_ne_one {a : α} : s.mulIndicator f a ≠ 1s.mulIndicator f a ≠ 1 ↔ a ∈ s ∩ mulSupport f := by
  simp only [Ne, mulIndicator_apply_eq_one, Classical.not_imp, mem_inter_iff, mem_mulSupport]
Non-identity Condition for Multiplicative Indicator Function
Informal description
For any element $a \in \alpha$, the multiplicative indicator function $\text{mulIndicator}_s f$ evaluated at $a$ is not equal to $1$ if and only if $a$ belongs to both the set $s$ and the multiplicative support of $f$. In other words: \[ \text{mulIndicator}_s f (a) \neq 1 \leftrightarrow a \in s \cap \text{mulSupport}(f), \] where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$.
Set.mulSupport_mulIndicator theorem
: Function.mulSupport (s.mulIndicator f) = s ∩ Function.mulSupport f
Full source 
@[to_additive (attr := simp)]
theorem mulSupport_mulIndicator :
    Function.mulSupport (s.mulIndicator f) = s ∩ Function.mulSupport f :=
  ext fun x => by simp [Function.mem_mulSupport, mulIndicator_apply_eq_one]
Multiplicative Support of Multiplicative Indicator Function
Informal description
For any set $s \subseteq \alpha$ and function $f : \alpha \to M$, the multiplicative support of the multiplicative indicator function $\text{mulIndicator}_s f$ is equal to the intersection of $s$ with the multiplicative support of $f$. In other words: \[ \text{mulSupport}(\text{mulIndicator}_s f) = s \cap \text{mulSupport}(f) \] where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$.
Set.mem_of_mulIndicator_ne_one theorem
(h : mulIndicator s f a ≠ 1) : a ∈ s
Full source 
/-- If a multiplicative indicator function is not equal to `1` at a point, then that point is in the
set. -/
@[to_additive
      "If an additive indicator function is not equal to `0` at a point, then that point is
      in the set."]
theorem mem_of_mulIndicator_ne_one (h : mulIndicatormulIndicator s f a ≠ 1) : a ∈ s :=
  not_imp_comm.1 (fun hn => mulIndicator_of_not_mem hn f) h
Membership from Non-identity of Multiplicative Indicator Function
Informal description
For a set $s \subseteq \alpha$, a function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), and an element $a \in \alpha$, if the multiplicative indicator function $\text{mulIndicator}_s f$ evaluated at $a$ is not equal to $1$, then $a$ belongs to $s$. In other words: \[ \text{mulIndicator}_s f (a) \neq 1 \implies a \in s. \]
Set.eqOn_mulIndicator theorem
: EqOn (mulIndicator s f) f s
Full source 
/-- See `Set.eqOn_mulIndicator'` for the version with `sᶜ`. -/
@[to_additive
      "See `Set.eqOn_indicator'` for the version with `sᶜ`"]
theorem eqOn_mulIndicator : EqOn (mulIndicator s f) f s := fun _ hx => mulIndicator_of_mem hx f
Multiplicative Indicator Function Equals Original Function on Set
Informal description
For a set $s \subseteq \alpha$ and a function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative indicator function $\text{mulIndicator}_s f$ coincides with $f$ on the set $s$. That is, for all $x \in s$, we have: \[ \text{mulIndicator}_s f (x) = f(x). \]
Set.eqOn_mulIndicator' theorem
: EqOn (mulIndicator s f) 1 sᶜ
Full source 
/-- See `Set.eqOn_mulIndicator` for the version with `s`. -/
@[to_additive
      "See `Set.eqOn_indicator` for the version with `s`."]
theorem eqOn_mulIndicator' : EqOn (mulIndicator s f) 1 sᶜ :=
  fun _ hx => mulIndicator_of_not_mem hx f
Multiplicative Indicator Equals One on Complement
Informal description
For a set $s \subseteq \alpha$ and a function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative indicator function $\text{mulIndicator}_s f$ coincides with the constant function $1$ on the complement set $s^c$. That is, for all $x \in s^c$, we have: \[ \text{mulIndicator}_s f (x) = 1. \]
Set.mulSupport_mulIndicator_subset theorem
: mulSupport (s.mulIndicator f) ⊆ s
Full source 
@[to_additive]
theorem mulSupport_mulIndicator_subset : mulSupportmulSupport (s.mulIndicator f) ⊆ s := fun _ hx =>
  hx.imp_symm fun h => mulIndicator_of_not_mem h f
Multiplicative Support of Indicator Function is Contained in Set
Informal description
For any set $s \subseteq \alpha$ and any function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative support of the multiplicative indicator function $\text{mulIndicator}_s f$ is a subset of $s$. In other words, \[ \{x \in \alpha \mid \text{mulIndicator}_s f (x) \neq 1\} \subseteq s. \]
Set.mulIndicator_mulSupport theorem
: mulIndicator (mulSupport f) f = f
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_mulSupport : mulIndicator (mulSupport f) f = f :=
  mulIndicator_eq_self.2 Subset.rfl
Multiplicative Indicator Function Equals Original on Its Support
Informal description
For any function $f \colon \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative indicator function of $f$ over its multiplicative support equals $f$ itself. That is, \[ \text{mulIndicator}_{\text{mulSupport}(f)} f = f, \] where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$.
Set.mulIndicator_range_comp theorem
{ι : Sort*} (f : ι → α) (g : α → M) : mulIndicator (range f) g ∘ f = g ∘ f
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_range_comp {ι : Sort*} (f : ι → α) (g : α → M) :
    mulIndicatormulIndicator (range f) g ∘ f = g ∘ f :=
  letI := Classical.decPred (· ∈ range f)
  piecewise_range_comp _ _ _
Composition of Multiplicative Indicator Function with Range
Informal description
For any function $f \colon \iota \to \alpha$ and any function $g \colon \alpha \to M$, the composition of the multiplicative indicator function of $g$ over the range of $f$ with $f$ equals the composition of $g$ with $f$. That is, \[ \text{mulIndicator}_{\text{range}\, f}\, g \circ f = g \circ f. \]
Set.mulIndicator_congr theorem
(h : EqOn f g s) : mulIndicator s f = mulIndicator s g
Full source 
@[to_additive]
theorem mulIndicator_congr (h : EqOn f g s) : mulIndicator s f = mulIndicator s g :=
  funext fun x => by
    simp only [mulIndicator]
    split_ifs with h_1
    · exact h h_1
    rfl
Equality of Multiplicative Indicator Functions for Coinciding Functions
Informal description
For any set $s \subseteq \alpha$ and functions $f, g : \alpha \to M$ that agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), the multiplicative indicator functions $\text{mulIndicator}_s f$ and $\text{mulIndicator}_s g$ are equal.
Set.mulIndicator_eq_mulIndicator theorem
{t : Set β} {g : β → M} {b : β} (h1 : a ∈ s ↔ b ∈ t) (h2 : f a = g b) : s.mulIndicator f a = t.mulIndicator g b
Full source 
@[to_additive]
theorem mulIndicator_eq_mulIndicator {t : Set β} {g : β → M} {b : β}
    (h1 : a ∈ sa ∈ s ↔ b ∈ t) (h2 : f a = g b) :
    s.mulIndicator f a = t.mulIndicator g b := by
  by_cases a ∈ s <;> simp_all
Equality of Multiplicative Indicator Functions Under Correspondence
Informal description
For sets $s \subseteq \alpha$ and $t \subseteq \beta$, functions $f : \alpha \to M$ and $g : \beta \to M$ (where $M$ has a multiplicative identity $1$), and elements $a \in \alpha$, $b \in \beta$ such that: 1. $a \in s$ if and only if $b \in t$, and 2. $f(a) = g(b)$, then the multiplicative indicator functions satisfy: \[ \text{mulIndicator}_s f (a) = \text{mulIndicator}_t g (b). \]
Set.mulIndicator_const_eq_mulIndicator_const theorem
{t : Set β} {b : β} {c : M} (h : a ∈ s ↔ b ∈ t) : s.mulIndicator (fun _ ↦ c) a = t.mulIndicator (fun _ ↦ c) b
Full source 
@[to_additive]
theorem mulIndicator_const_eq_mulIndicator_const {t : Set β} {b : β} {c : M} (h : a ∈ sa ∈ s ↔ b ∈ t) :
    s.mulIndicator (fun _ ↦ c) a = t.mulIndicator (fun _ ↦ c) b :=
  mulIndicator_eq_mulIndicator h rfl
Equality of Constant Multiplicative Indicator Functions Under Set Correspondence
Informal description
For sets $s \subseteq \alpha$ and $t \subseteq \beta$, a constant $c \in M$ (where $M$ has a multiplicative identity $1$), and elements $a \in \alpha$, $b \in \beta$ such that $a \in s$ if and only if $b \in t$, the multiplicative indicator functions satisfy: \[ \text{mulIndicator}_s (\lambda \_\mapsto c) (a) = \text{mulIndicator}_t (\lambda \_\mapsto c) (b). \]
Set.mulIndicator_univ theorem
(f : α → M) : mulIndicator (univ : Set α) f = f
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_univ (f : α → M) : mulIndicator (univ : Set α) f = f :=
  mulIndicator_eq_self.2 <| subset_univ _
Multiplicative Indicator on Universal Set Equals Original Function
Informal description
For any function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative indicator function on the universal set $\text{univ} \subseteq \alpha$ equals $f$, i.e., \[ \text{mulIndicator}_{\text{univ}} f = f. \]
Set.mulIndicator_empty theorem
(f : α → M) : mulIndicator (∅ : Set α) f = fun _ => 1
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_empty (f : α → M) : mulIndicator (∅ : Set α) f = fun _ => 1 :=
  mulIndicator_eq_one.2 <| disjoint_empty _
Multiplicative Indicator on Empty Set is Constant One Function
Informal description
For any function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative indicator function on the empty set $\emptyset \subseteq \alpha$ is equal to the constant function $1$, i.e., \[ \text{mulIndicator}_{\emptyset} f = \mathbf{1}, \] where $\mathbf{1}$ denotes the constant function $x \mapsto 1$.
Set.mulIndicator_empty' theorem
(f : α → M) : mulIndicator (∅ : Set α) f = 1
Full source 
@[to_additive]
theorem mulIndicator_empty' (f : α → M) : mulIndicator (∅ : Set α) f = 1 :=
  mulIndicator_empty f
Multiplicative Indicator on Empty Set is Constant One
Informal description
For any function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative indicator function on the empty set $\emptyset \subseteq \alpha$ is equal to the constant function $1$, i.e., \[ \text{mulIndicator}_{\emptyset} f = 1. \]
Set.mulIndicator_one theorem
(s : Set α) : (mulIndicator s fun _ => (1 : M)) = fun _ => (1 : M)
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_one (s : Set α) : (mulIndicator s fun _ => (1 : M)) = fun _ => (1 : M) :=
  mulIndicator_eq_one.2 <| by simp only [mulSupport_one, empty_disjoint]
Multiplicative Indicator of Constant One Function is Constant One
Informal description
For any set $s \subseteq \alpha$ and the constant function $f : \alpha \to M$ defined by $f(x) = 1$ for all $x \in \alpha$, the multiplicative indicator function $\text{mulIndicator}_s f$ is equal to the constant function $1$. That is: \[ \text{mulIndicator}_s (\mathbf{1}) = \mathbf{1}, \] where $\mathbf{1}$ denotes the constant function $x \mapsto 1$.
Set.mulIndicator_one' theorem
{s : Set α} : s.mulIndicator (1 : α → M) = 1
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_one' {s : Set α} : s.mulIndicator (1 : α → M) = 1 :=
  mulIndicator_one M s
Multiplicative Indicator of Constant One Function is Constant One
Informal description
For any set $s \subseteq \alpha$, the multiplicative indicator function of $s$ applied to the constant function $1$ is equal to the constant function $1$. That is, \[ \text{mulIndicator}_s (\mathbf{1}) = \mathbf{1}, \] where $\mathbf{1}$ denotes the constant function $x \mapsto 1$.
Set.mulIndicator_mulIndicator theorem
(s t : Set α) (f : α → M) : mulIndicator s (mulIndicator t f) = mulIndicator (s ∩ t) f
Full source 
@[to_additive]
theorem mulIndicator_mulIndicator (s t : Set α) (f : α → M) :
    mulIndicator s (mulIndicator t f) = mulIndicator (s ∩ t) f :=
  funext fun x => by
    simp only [mulIndicator]
    split_ifs <;> simp_all +contextual
Composition of Multiplicative Indicator Functions over Intersection
Informal description
For any sets $s, t \subseteq \alpha$ and any function $f : \alpha \to M$, the multiplicative indicator function of $s$ applied to the multiplicative indicator function of $t$ applied to $f$ is equal to the multiplicative indicator function of the intersection $s \cap t$ applied to $f$. That is: \[ \text{mulIndicator}_s (\text{mulIndicator}_t f) = \text{mulIndicator}_{s \cap t} f \]
Set.mulIndicator_inter_mulSupport theorem
(s : Set α) (f : α → M) : mulIndicator (s ∩ mulSupport f) f = mulIndicator s f
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_inter_mulSupport (s : Set α) (f : α → M) :
    mulIndicator (s ∩ mulSupport f) f = mulIndicator s f := by
  rw [← mulIndicator_mulIndicator, mulIndicator_mulSupport]
Multiplicative Indicator Function Equality on Intersection with Support
Informal description
For any set $s \subseteq \alpha$ and any function $f \colon \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative indicator function of $f$ over the intersection of $s$ with the multiplicative support of $f$ equals the multiplicative indicator function of $f$ over $s$. That is, \[ \text{mulIndicator}_{s \cap \text{mulSupport}(f)} f = \text{mulIndicator}_s f, \] where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$.
Set.comp_mulIndicator theorem
(h : M → β) (f : α → M) {s : Set α} {x : α} [DecidablePred (· ∈ s)] : h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x
Full source 
@[to_additive]
theorem comp_mulIndicator (h : M → β) (f : α → M) {s : Set α} {x : α} [DecidablePred (· ∈ s)] :
    h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x := by
  letI := Classical.decPred (· ∈ s)
  convert s.apply_piecewise f (const α 1) (fun _ => h) (x := x) using 2
Composition with Multiplicative Indicator Function
Informal description
Let $h : M \to \beta$ be a function, $f : \alpha \to M$ be another function, and $s \subseteq \alpha$ be a set. For any $x \in \alpha$, we have: \[ h \left( \text{mulIndicator}_s f \, x \right) = \begin{cases} h(f(x)) & \text{if } x \in s, \\ h(1) & \text{otherwise}, \end{cases} \] where $\text{mulIndicator}_s f$ is the multiplicative indicator function of $f$ on $s$, defined as $f(x)$ if $x \in s$ and $1$ otherwise.
Set.mulIndicator_comp_right theorem
{s : Set α} (f : β → α) {g : α → M} {x : β} : mulIndicator (f ⁻¹' s) (g ∘ f) x = mulIndicator s g (f x)
Full source 
@[to_additive]
theorem mulIndicator_comp_right {s : Set α} (f : β → α) {g : α → M} {x : β} :
    mulIndicator (f ⁻¹' s) (g ∘ f) x = mulIndicator s g (f x) := by
  simp only [mulIndicator, Function.comp]
  split_ifs with h h' h'' <;> first | rfl | contradiction
Composition Rule for Multiplicative Indicator Function via Preimage
Informal description
For any set $s \subseteq \alpha$, function $f : \beta \to \alpha$, function $g : \alpha \to M$, and point $x \in \beta$, the multiplicative indicator function satisfies: \[ \text{mulIndicator}_{f^{-1}(s)} (g \circ f) \, x = \text{mulIndicator}_s g \, (f x) \] where $\text{mulIndicator}_s g$ is defined as $g(y)$ if $y \in s$ and $1$ otherwise, and $f^{-1}(s)$ denotes the preimage of $s$ under $f$.
Set.mulIndicator_image theorem
{s : Set α} {f : β → M} {g : α → β} (hg : Injective g) {x : α} : mulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) x
Full source 
@[to_additive]
theorem mulIndicator_image {s : Set α} {f : β → M} {g : α → β} (hg : Injective g) {x : α} :
    mulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) x := by
  rw [← mulIndicator_comp_right, preimage_image_eq _ hg]
Multiplicative Indicator Function under Injective Image: $\text{mulIndicator}_{g(s)} f \circ g = \text{mulIndicator}_s (f \circ g)$
Informal description
For any set $s \subseteq \alpha$, function $f : \beta \to M$, and injective function $g : \alpha \to \beta$, the multiplicative indicator function satisfies: \[ \text{mulIndicator}_{g(s)} f \, (g x) = \text{mulIndicator}_s (f \circ g) \, x \] for all $x \in \alpha$, where $g(s)$ denotes the image of $s$ under $g$, and $\text{mulIndicator}_s h$ is defined as $h(y)$ if $y \in s$ and $1$ otherwise.
Set.mulIndicator_comp_of_one theorem
{g : M → N} (hg : g 1 = 1) : mulIndicator s (g ∘ f) = g ∘ mulIndicator s f
Full source 
@[to_additive]
theorem mulIndicator_comp_of_one {g : M → N} (hg : g 1 = 1) :
    mulIndicator s (g ∘ f) = g ∘ mulIndicator s f := by
  funext
  simp only [mulIndicator]
  split_ifs <;> simp [*]
Composition Rule for Multiplicative Indicator Function with $g(1) = 1$
Informal description
For any function $g \colon M \to N$ satisfying $g(1) = 1$, the multiplicative indicator function of the composition $g \circ f$ on a set $s$ is equal to the composition of $g$ with the multiplicative indicator function of $f$ on $s$, i.e., \[ \text{mulIndicator}_s (g \circ f) = g \circ \text{mulIndicator}_s f. \]
Set.comp_mulIndicator_const theorem
(c : M) (f : M → N) (hf : f 1 = 1) : (fun x => f (s.mulIndicator (fun _ => c) x)) = s.mulIndicator fun _ => f c
Full source 
@[to_additive]
theorem comp_mulIndicator_const (c : M) (f : M → N) (hf : f 1 = 1) :
    (fun x => f (s.mulIndicator (fun _ => c) x)) = s.mulIndicator fun _ => f c :=
  (mulIndicator_comp_of_one hf).symm
Composition of Function with Constant Multiplicative Indicator Function
Informal description
For any constant $c \in M$ and any function $f \colon M \to N$ satisfying $f(1) = 1$, the composition of $f$ with the multiplicative indicator function of the constant function $\lambda \_, c$ on a set $s$ is equal to the multiplicative indicator function of the constant function $\lambda \_, f(c)$ on $s$. That is, \[ f \circ (\text{mulIndicator}_s (\lambda \_, c)) = \text{mulIndicator}_s (\lambda \_, f(c)). \]
Set.mulIndicator_preimage theorem
(s : Set α) (f : α → M) (B : Set M) : mulIndicator s f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B)
Full source 
@[to_additive]
theorem mulIndicator_preimage (s : Set α) (f : α → M) (B : Set M) :
    mulIndicatormulIndicator s f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B) :=
  letI := Classical.decPred (· ∈ s)
  piecewise_preimage s f 1 B
Preimage of Multiplicative Indicator Function
Informal description
For any set $s \subseteq \alpha$, function $f \colon \alpha \to M$, and subset $B \subseteq M$, the preimage of $B$ under the multiplicative indicator function $\text{mulIndicator}_s f$ is equal to the set defined by: \[ (\text{mulIndicator}_s f)^{-1}(B) = \begin{cases} f^{-1}(B) & \text{if } x \in s, \\ 1^{-1}(B) & \text{otherwise.} \end{cases} \] Here, $1^{-1}(B)$ denotes the preimage of $B$ under the constant function that maps every element to the multiplicative identity $1 \in M$.
Set.mulIndicator_one_preimage theorem
(s : Set M) : t.mulIndicator 1 ⁻¹' s ∈ ({Set.univ, ∅} : Set (Set α))
Full source 
@[to_additive]
theorem mulIndicator_one_preimage (s : Set M) :
    t.mulIndicator 1 ⁻¹' st.mulIndicator 1 ⁻¹' s ∈ ({Set.univ, ∅} : Set (Set α)) := by
  classical
    rw [mulIndicator_one', preimage_one]
    split_ifs <;> simp
Preimage of Multiplicative Indicator of Constant One Function is Universal or Empty
Informal description
For any set $s \subseteq M$, the preimage of $s$ under the multiplicative indicator function of a set $t$ applied to the constant function $1$ is either the universal set or the empty set. That is, \[ (\text{mulIndicator}_t \mathbf{1})^{-1}(s) \in \{\alpha, \emptyset\}, \] where $\mathbf{1}$ denotes the constant function $x \mapsto 1$.
Set.mulIndicator_const_preimage_eq_union theorem
(U : Set α) (s : Set M) (a : M) [Decidable (a ∈ s)] [Decidable ((1 : M) ∈ s)] : (U.mulIndicator fun _ => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if (1 : M) ∈ s then Uᶜ else ∅
Full source 
@[to_additive]
theorem mulIndicator_const_preimage_eq_union (U : Set α) (s : Set M) (a : M) [Decidable (a ∈ s)]
    [Decidable ((1 : M) ∈ s)] : (U.mulIndicator fun _ => a) ⁻¹' s =
      (if a ∈ s then U else ∅) ∪ if (1 : M) ∈ s then Uᶜ else ∅ := by
  rw [mulIndicator_preimage, preimage_one, preimage_const]
  split_ifs <;> simp [← compl_eq_univ_diff]
Preimage of Constant Multiplicative Indicator Function as Union of Conditional Sets
Informal description
For any set $U \subseteq \alpha$, subset $s \subseteq M$, and element $a \in M$, the preimage of $s$ under the multiplicative indicator function of $U$ with constant value $a$ is given by: \[ (U.\text{mulIndicator} \, (\lambda \_ \mapsto a))^{-1}(s) = \begin{cases} U & \text{if } a \in s, \\ \emptyset & \text{otherwise} \end{cases} \cup \begin{cases} U^c & \text{if } 1 \in s, \\ \emptyset & \text{otherwise.} \end{cases} \] Here, $1$ denotes the multiplicative identity in $M$, and $U^c$ is the complement of $U$ in $\alpha$.
Set.mulIndicator_const_preimage theorem
(U : Set α) (s : Set M) (a : M) : (U.mulIndicator fun _ => a) ⁻¹' s ∈ ({Set.univ, U, Uᶜ, ∅} : Set (Set α))
Full source 
@[to_additive]
theorem mulIndicator_const_preimage (U : Set α) (s : Set M) (a : M) :
    (U.mulIndicator fun _ => a) ⁻¹' s(U.mulIndicator fun _ => a) ⁻¹' s ∈ ({Set.univ, U, Uᶜ, ∅} : Set (Set α)) := by
  classical
    rw [mulIndicator_const_preimage_eq_union]
    split_ifs <;> simp
Possible Preimages of Constant Multiplicative Indicator Function
Informal description
For any set $U \subseteq \alpha$, subset $s \subseteq M$, and element $a \in M$, the preimage of $s$ under the multiplicative indicator function of $U$ with constant value $a$ is one of the following sets: the universal set $\alpha$, $U$, its complement $U^c$, or the empty set $\emptyset$.
Set.indicator_one_preimage theorem
[Zero M] (U : Set α) (s : Set M) : U.indicator 1 ⁻¹' s ∈ ({Set.univ, U, Uᶜ, ∅} : Set (Set α))
Full source 
theorem indicator_one_preimage [Zero M] (U : Set α) (s : Set M) :
    U.indicator 1 ⁻¹' sU.indicator 1 ⁻¹' s ∈ ({Set.univ, U, Uᶜ, ∅} : Set (Set α)) :=
  indicator_const_preimage _ _ 1
Possible Preimages of Constant Indicator Function with Value One
Informal description
For any set $U \subseteq \alpha$ and subset $s \subseteq M$ where $M$ has a zero element, the preimage of $s$ under the indicator function of $U$ with constant value $1$ (where $1$ is interpreted as the multiplicative identity in $M$) is one of the following sets: the universal set $\alpha$, $U$, its complement $U^c$, or the empty set $\emptyset$.
Set.mulIndicator_preimage_of_not_mem theorem
(s : Set α) (f : α → M) {t : Set M} (ht : (1 : M) ∉ t) : mulIndicator s f ⁻¹' t = f ⁻¹' t ∩ s
Full source 
@[to_additive]
theorem mulIndicator_preimage_of_not_mem (s : Set α) (f : α → M) {t : Set M} (ht : (1 : M) ∉ t) :
    mulIndicatormulIndicator s f ⁻¹' t = f ⁻¹' tf ⁻¹' t ∩ s := by
  simp [mulIndicator_preimage, Pi.one_def, Set.preimage_const_of_not_mem ht]
Preimage of Multiplicative Indicator Function Excluding Identity
Informal description
For any set $s \subseteq \alpha$, function $f \colon \alpha \to M$, and subset $t \subseteq M$ such that $1 \notin t$, the preimage of $t$ under the multiplicative indicator function $\text{mulIndicator}_s f$ is equal to the intersection of the preimage of $t$ under $f$ with $s$. That is, \[ (\text{mulIndicator}_s f)^{-1}(t) = f^{-1}(t) \cap s. \]
Set.mem_range_mulIndicator theorem
{r : M} {s : Set α} {f : α → M} : r ∈ range (mulIndicator s f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s
Full source 
@[to_additive]
theorem mem_range_mulIndicator {r : M} {s : Set α} {f : α → M} :
    r ∈ range (mulIndicator s f)r ∈ range (mulIndicator s f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s := by
  simp [mulIndicator, ite_eq_iff, exists_or, eq_univ_iff_forall, and_comm, or_comm,
    @eq_comm _ r 1]
Characterization of the Range of a Multiplicative Indicator Function
Informal description
For any element $r \in M$, set $s \subseteq \alpha$, and function $f : \alpha \to M$, the element $r$ is in the range of the multiplicative indicator function $\text{mulIndicator}_s f$ if and only if either $r = 1$ and $s \neq \alpha$, or $r$ is in the image of $f$ restricted to $s$.
Set.mulIndicator_rel_mulIndicator theorem
{r : M → M → Prop} (h1 : r 1 1) (ha : a ∈ s → r (f a) (g a)) : r (mulIndicator s f a) (mulIndicator s g a)
Full source 
@[to_additive]
theorem mulIndicator_rel_mulIndicator {r : M → M → Prop} (h1 : r 1 1) (ha : a ∈ s → r (f a) (g a)) :
    r (mulIndicator s f a) (mulIndicator s g a) := by
  simp only [mulIndicator]
  split_ifs with has
  exacts [ha has, h1]
Relation Preservation by Multiplicative Indicator Functions
Informal description
Let $M$ be a type with a multiplicative identity $1$, and let $r : M \to M \to \mathrm{Prop}$ be a relation such that $r(1,1)$ holds. For any set $s \subseteq \alpha$, functions $f, g : \alpha \to M$, and element $a \in \alpha$, if $r(f(a), g(a))$ holds whenever $a \in s$, then $r(\text{mulIndicator}_s f(a), \text{mulIndicator}_s g(a))$ holds, where $\text{mulIndicator}_s f$ is the multiplicative indicator function of $f$ on $s$.
Set.mulIndicator_union_mul_inter_apply theorem
(f : α → M) (s t : Set α) (a : α) : mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a
Full source 
@[to_additive]
theorem mulIndicator_union_mul_inter_apply (f : α → M) (s t : Set α) (a : α) :
    mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a
      = mulIndicator s f a * mulIndicator t f a := by
  by_cases hs : a ∈ s <;> by_cases ht : a ∈ t <;> simp [*]
Product of Multiplicative Indicators on Union and Intersection Equals Product on Individual Sets
Informal description
For any function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), sets $s, t \subseteq \alpha$, and element $a \in \alpha$, the following identity holds: \[ \text{mulIndicator}_{s \cup t} f (a) \cdot \text{mulIndicator}_{s \cap t} f (a) = \text{mulIndicator}_s f (a) \cdot \text{mulIndicator}_t f (a). \] Here, $\text{mulIndicator}_S f (x)$ denotes the multiplicative indicator function, which equals $f(x)$ if $x \in S$ and $1$ otherwise.
Set.mulIndicator_union_mul_inter theorem
(f : α → M) (s t : Set α) : mulIndicator (s ∪ t) f * mulIndicator (s ∩ t) f = mulIndicator s f * mulIndicator t f
Full source 
@[to_additive]
theorem mulIndicator_union_mul_inter (f : α → M) (s t : Set α) :
    mulIndicator (s ∪ t) f * mulIndicator (s ∩ t) f = mulIndicator s f * mulIndicator t f :=
  funext <| mulIndicator_union_mul_inter_apply f s t
Product of Multiplicative Indicators on Union and Intersection Equals Product on Individual Sets
Informal description
For any function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$) and any sets $s, t \subseteq \alpha$, the following identity holds: \[ \text{mulIndicator}_{s \cup t} f \cdot \text{mulIndicator}_{s \cap t} f = \text{mulIndicator}_s f \cdot \text{mulIndicator}_t f. \] Here, $\text{mulIndicator}_S f$ denotes the multiplicative indicator function, which equals $f(x)$ if $x \in S$ and $1$ otherwise.
Set.mulIndicator_union_of_not_mem_inter theorem
(h : a ∉ s ∩ t) (f : α → M) : mulIndicator (s ∪ t) f a = mulIndicator s f a * mulIndicator t f a
Full source 
@[to_additive]
theorem mulIndicator_union_of_not_mem_inter (h : a ∉ s ∩ t) (f : α → M) :
    mulIndicator (s ∪ t) f a = mulIndicator s f a * mulIndicator t f a := by
  rw [← mulIndicator_union_mul_inter_apply f s t, mulIndicator_of_not_mem h, mul_one]
Multiplicative Indicator on Union for Elements Outside Intersection: \(\text{mulIndicator}_{s \cup t} f (a) = \text{mulIndicator}_s f (a) \cdot \text{mulIndicator}_t f (a)\) when \(a \notin s \cap t\)
Informal description
For a function \( f : \alpha \to M \) (where \( M \) has a multiplicative identity \( 1 \)), sets \( s, t \subseteq \alpha \), and an element \( a \in \alpha \) such that \( a \notin s \cap t \), the multiplicative indicator function satisfies: \[ \text{mulIndicator}_{s \cup t} f (a) = \text{mulIndicator}_s f (a) \cdot \text{mulIndicator}_t f (a). \] Here, \(\text{mulIndicator}_S f (x)\) denotes the multiplicative indicator function, which equals \(f(x)\) if \(x \in S\) and \(1\) otherwise.
Set.mulIndicator_union_of_disjoint theorem
(h : Disjoint s t) (f : α → M) : mulIndicator (s ∪ t) f = fun a => mulIndicator s f a * mulIndicator t f a
Full source 
@[to_additive]
theorem mulIndicator_union_of_disjoint (h : Disjoint s t) (f : α → M) :
    mulIndicator (s ∪ t) f = fun a => mulIndicator s f a * mulIndicator t f a :=
  funext fun _ => mulIndicator_union_of_not_mem_inter (fun ha => h.le_bot ha) _
Multiplicative Indicator on Union of Disjoint Sets: $\text{mulIndicator}_{s \cup t} f = \text{mulIndicator}_s f \cdot \text{mulIndicator}_t f$
Informal description
For any function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$) and any disjoint sets $s, t \subseteq \alpha$, the multiplicative indicator function satisfies: \[ \text{mulIndicator}_{s \cup t} f (a) = \text{mulIndicator}_s f (a) \cdot \text{mulIndicator}_t f (a) \] for all $a \in \alpha$, where $\text{mulIndicator}_S f (x) = f(x)$ if $x \in S$ and $1$ otherwise.
Set.mulIndicator_symmDiff theorem
(s t : Set α) (f : α → M) : mulIndicator (s ∆ t) f = mulIndicator (s \ t) f * mulIndicator (t \ s) f
Full source 
@[to_additive]
theorem mulIndicator_symmDiff (s t : Set α) (f : α → M) :
    mulIndicator (s ∆ t) f = mulIndicator (s \ t) f * mulIndicator (t \ s) f :=
  mulIndicator_union_of_disjoint (disjoint_sdiff_self_right.mono_left sdiff_le) _
Multiplicative Indicator on Symmetric Difference: $\text{mulIndicator}_{s \Delta t} f = \text{mulIndicator}_{s \setminus t} f \cdot \text{mulIndicator}_{t \setminus s} f$
Informal description
For any sets $s, t \subseteq \alpha$ and function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the multiplicative indicator function on the symmetric difference $s \Delta t$ satisfies: \[ \text{mulIndicator}_{s \Delta t} f = \text{mulIndicator}_{s \setminus t} f \cdot \text{mulIndicator}_{t \setminus s} f \] where $\text{mulIndicator}_S f(x) = f(x)$ if $x \in S$ and $1$ otherwise, and $\cdot$ denotes pointwise multiplication.
Set.mulIndicator_mul theorem
(s : Set α) (f g : α → M) : (mulIndicator s fun a => f a * g a) = fun a => mulIndicator s f a * mulIndicator s g a
Full source 
@[to_additive]
theorem mulIndicator_mul (s : Set α) (f g : α → M) :
    (mulIndicator s fun a => f a * g a) = fun a => mulIndicator s f a * mulIndicator s g a := by
  funext
  simp only [mulIndicator]
  split_ifs
  · rfl
  rw [mul_one]
Multiplicative indicator preserves pointwise multiplication: $\text{mulIndicator}_s (f \cdot g) = \text{mulIndicator}_s f \cdot \text{mulIndicator}_s g$
Informal description
For any set $s \subseteq \alpha$ and functions $f, g : \alpha \to M$, the multiplicative indicator function satisfies: \[ \text{mulIndicator}_s (f \cdot g) = \text{mulIndicator}_s f \cdot \text{mulIndicator}_s g \] where $\text{mulIndicator}_s h(x) = h(x)$ if $x \in s$ and $1$ otherwise, and $\cdot$ denotes pointwise multiplication.
Set.mulIndicator_mul' theorem
(s : Set α) (f g : α → M) : mulIndicator s (f * g) = mulIndicator s f * mulIndicator s g
Full source 
@[to_additive]
theorem mulIndicator_mul' (s : Set α) (f g : α → M) :
    mulIndicator s (f * g) = mulIndicator s f * mulIndicator s g :=
  mulIndicator_mul s f g
Multiplicative Indicator Preserves Pointwise Multiplication: $\text{mulIndicator}_s (f \cdot g) = \text{mulIndicator}_s f \cdot \text{mulIndicator}_s g$
Informal description
For any set $s \subseteq \alpha$ and functions $f, g : \alpha \to M$, the multiplicative indicator function satisfies: \[ \text{mulIndicator}_s (f \cdot g) = \text{mulIndicator}_s f \cdot \text{mulIndicator}_s g \] where $\text{mulIndicator}_s h(x) = h(x)$ if $x \in s$ and $1$ otherwise, and $\cdot$ denotes pointwise multiplication.
Set.mulIndicator_compl_mul_self_apply theorem
(s : Set α) (f : α → M) (a : α) : mulIndicator sᶜ f a * mulIndicator s f a = f a
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_compl_mul_self_apply (s : Set α) (f : α → M) (a : α) :
    mulIndicator sᶜ f a * mulIndicator s f a = f a :=
  by_cases (fun ha : a ∈ s => by simp [ha]) fun ha => by simp [ha]
Product of Complementary Multiplicative Indicators Equals Original Function
Informal description
For any set $s \subseteq \alpha$, function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), and element $a \in \alpha$, the product of the multiplicative indicator functions of the complement of $s$ and $s$ itself evaluated at $a$ equals $f(a)$. That is: \[ \text{mulIndicator}_{s^c} f (a) \cdot \text{mulIndicator}_s f (a) = f(a). \]
Set.mulIndicator_compl_mul_self theorem
(s : Set α) (f : α → M) : mulIndicator sᶜ f * mulIndicator s f = f
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_compl_mul_self (s : Set α) (f : α → M) :
    mulIndicator sᶜ f * mulIndicator s f = f :=
  funext <| mulIndicator_compl_mul_self_apply s f
Product of Complementary Multiplicative Indicators Equals Original Function
Informal description
For any set $s \subseteq \alpha$ and function $f : \alpha \to M$ (where $M$ is a type with multiplicative identity $1$), the product of the multiplicative indicator functions of the complement $s^c$ and $s$ equals $f$. That is: \[ \text{mulIndicator}_{s^c} f \cdot \text{mulIndicator}_s f = f. \]
Set.mulIndicator_self_mul_compl_apply theorem
(s : Set α) (f : α → M) (a : α) : mulIndicator s f a * mulIndicator sᶜ f a = f a
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_self_mul_compl_apply (s : Set α) (f : α → M) (a : α) :
    mulIndicator s f a * mulIndicator sᶜ f a = f a :=
  by_cases (fun ha : a ∈ s => by simp [ha]) fun ha => by simp [ha]
Product of Multiplicative Indicators Equals Original Function
Informal description
For any set $s \subseteq \alpha$, function $f : \alpha \to M$ (where $M$ has a multiplicative identity $1$), and element $a \in \alpha$, the product of the multiplicative indicator functions of $s$ and its complement $sᶜ$ evaluated at $a$ equals $f(a)$. That is: \[ \text{mulIndicator}_s f (a) \cdot \text{mulIndicator}_{sᶜ} f (a) = f(a). \]
Set.mulIndicator_self_mul_compl theorem
(s : Set α) (f : α → M) : mulIndicator s f * mulIndicator sᶜ f = f
Full source 
@[to_additive (attr := simp)]
theorem mulIndicator_self_mul_compl (s : Set α) (f : α → M) :
    mulIndicator s f * mulIndicator sᶜ f = f :=
  funext <| mulIndicator_self_mul_compl_apply s f
Product of Multiplicative Indicators Equals Original Function
Informal description
For any set $s \subseteq \alpha$ and function $f : \alpha \to M$ (where $M$ is a type with multiplicative identity $1$), the product of the multiplicative indicator functions of $s$ and its complement $s^c$ equals $f$. That is: \[ \text{mulIndicator}_s f \cdot \text{mulIndicator}_{s^c} f = f. \]
Set.mulIndicator_mul_eq_left theorem
{f g : α → M} (h : Disjoint (mulSupport f) (mulSupport g)) : (mulSupport f).mulIndicator (f * g) = f
Full source 
@[to_additive]
theorem mulIndicator_mul_eq_left {f g : α → M} (h : Disjoint (mulSupport f) (mulSupport g)) :
    (mulSupport f).mulIndicator (f * g) = f := by
  refine (mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport
  have : g x = 1 := nmem_mulSupport.1 (disjoint_left.1 h hx)
  rw [Pi.mul_apply, this, mul_one]
Multiplicative Indicator of Product Equals First Factor on Disjoint Supports
Informal description
For any functions $f, g \colon \alpha \to M$ with disjoint multiplicative supports, the multiplicative indicator function of $f \cdot g$ over the support of $f$ equals $f$. That is, \[ \text{mulIndicator}_{\text{mulSupport}(f)} (f \cdot g) = f, \] where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$ and $\text{mulSupport}(f)$ is disjoint from $\text{mulSupport}(g)$.
Set.mulIndicator_mul_eq_right theorem
{f g : α → M} (h : Disjoint (mulSupport f) (mulSupport g)) : (mulSupport g).mulIndicator (f * g) = g
Full source 
@[to_additive]
theorem mulIndicator_mul_eq_right {f g : α → M} (h : Disjoint (mulSupport f) (mulSupport g)) :
    (mulSupport g).mulIndicator (f * g) = g := by
  refine (mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport
  have : f x = 1 := nmem_mulSupport.1 (disjoint_right.1 h hx)
  rw [Pi.mul_apply, this, one_mul]
Multiplicative Indicator of Product over Disjoint Support Equals Second Function
Informal description
For any functions $f, g : \alpha \to M$ with disjoint multiplicative supports, the multiplicative indicator function of the product $f \cdot g$ over the support of $g$ equals $g$. That is, \[ \text{mulIndicator}_{\text{mulSupport}(g)} (f \cdot g) = g. \]
Set.mulIndicator_mul_compl_eq_piecewise theorem
[DecidablePred (· ∈ s)] (f g : α → M) : s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise f g
Full source 
@[to_additive]
theorem mulIndicator_mul_compl_eq_piecewise [DecidablePred (· ∈ s)] (f g : α → M) :
    s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise f g := by
  ext x
  by_cases h : x ∈ s
  · rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
      Set.mulIndicator_of_not_mem (Set.not_mem_compl_iff.2 h), mul_one]
  · rw [piecewise_eq_of_not_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_not_mem h,
      Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]
Product of Multiplicative Indicators Equals Piecewise Function
Informal description
For a set $s \subseteq \alpha$ and functions $f, g : \alpha \to M$ (where $M$ has a multiplicative identity $1$), the product of the multiplicative indicator functions of $s$ and its complement $s^c$ equals the piecewise function defined by $f$ on $s$ and $g$ on $s^c$. That is: \[ \text{mulIndicator}_s f \cdot \text{mulIndicator}_{s^c} g = \text{piecewise}_s f g. \] Here, the condition $x \in s$ is decidable for each $x \in \alpha$.
Set.mulIndicatorHom definition
{α} (M) [MulOneClass M] (s : Set α) : (α → M) →* α → M
Full source 
/-- `Set.mulIndicator` as a `monoidHom`. -/
@[to_additive "`Set.indicator` as an `addMonoidHom`."]
noncomputable def mulIndicatorHom {α} (M) [MulOneClass M] (s : Set α) : (α → M) →* α → M where
  toFun := mulIndicator s
  map_one' := mulIndicator_one M s
  map_mul' := mulIndicator_mul s
Multiplicative indicator as a monoid homomorphism
Informal description
For a set \( s \subseteq \alpha \) and a monoid \( M \), the multiplicative indicator function \(\text{mulIndicator}_s\) is a monoid homomorphism from the function space \( \alpha \to M \) to itself. Specifically: - It maps a function \( f : \alpha \to M \) to the function \( \text{mulIndicator}_s f \), defined by: \[ \text{mulIndicator}_s f (x) = \begin{cases} f(x) & \text{if } x \in s, \\ 1 & \text{otherwise.} \end{cases} \] - It preserves the monoid structure, i.e., \(\text{mulIndicator}_s (f \cdot g) = \text{mulIndicator}_s f \cdot \text{mulIndicator}_s g\) and \(\text{mulIndicator}_s 1 = 1\), where \(1\) is the constant function \(x \mapsto 1\).
Set.mulIndicator_inv' theorem
(s : Set α) (f : α → G) : mulIndicator s f⁻¹ = (mulIndicator s f)⁻¹
Full source 
@[to_additive]
theorem mulIndicator_inv' (s : Set α) (f : α → G) : mulIndicator s f⁻¹ = (mulIndicator s f)⁻¹ :=
  (mulIndicatorHom G s).map_inv f
Inverse of Multiplicative Indicator Equals Multiplicative Indicator of Inverse
Informal description
For any set $s \subseteq \alpha$ and any function $f \colon \alpha \to G$ (where $G$ is a group), the multiplicative indicator function of $s$ applied to the pointwise inverse $f^{-1}$ is equal to the pointwise inverse of the multiplicative indicator function of $s$ applied to $f$. That is: \[ \text{mulIndicator}_s (f^{-1}) = (\text{mulIndicator}_s f)^{-1}. \] Here, $f^{-1}(x) = (f(x))^{-1}$ for all $x \in \alpha$, and the multiplicative indicator function is defined as: \[ \text{mulIndicator}_s f (x) = \begin{cases} f(x) & \text{if } x \in s, \\ 1 & \text{otherwise.} \end{cases} \]
Set.mulIndicator_inv theorem
(s : Set α) (f : α → G) : (mulIndicator s fun a => (f a)⁻¹) = fun a => (mulIndicator s f a)⁻¹
Full source 
@[to_additive]
theorem mulIndicator_inv (s : Set α) (f : α → G) :
    (mulIndicator s fun a => (f a)⁻¹) = fun a => (mulIndicator s f a)⁻¹ :=
  mulIndicator_inv' s f
Pointwise Inverse of Multiplicative Indicator Function
Informal description
For any set $s \subseteq \alpha$ and any function $f \colon \alpha \to G$ (where $G$ is a group), the multiplicative indicator function of $s$ applied to the pointwise inverse of $f$ is equal to the pointwise inverse of the multiplicative indicator function of $s$ applied to $f$. That is: \[ \text{mulIndicator}_s (f^{-1}) = (\text{mulIndicator}_s f)^{-1}. \] Here, $f^{-1}(x) = (f(x))^{-1}$ for all $x \in \alpha$, and the multiplicative indicator function is defined as: \[ \text{mulIndicator}_s f (x) = \begin{cases} f(x) & \text{if } x \in s, \\ 1 & \text{otherwise.} \end{cases} \]
Set.mulIndicator_div theorem
(s : Set α) (f g : α → G) : (mulIndicator s fun a => f a / g a) = fun a => mulIndicator s f a / mulIndicator s g a
Full source 
@[to_additive]
theorem mulIndicator_div (s : Set α) (f g : α → G) :
    (mulIndicator s fun a => f a / g a) = fun a => mulIndicator s f a / mulIndicator s g a :=
  (mulIndicatorHom G s).map_div f g
Multiplicative Indicator Preserves Pointwise Division
Informal description
For any set $s \subseteq \alpha$ and any functions $f, g \colon \alpha \to G$ (where $G$ is a group), the multiplicative indicator function of $s$ applied to the pointwise division $f/g$ is equal to the pointwise division of the multiplicative indicator functions of $s$ applied to $f$ and $g$. That is: \[ \text{mulIndicator}_s \left(\frac{f}{g}\right) = \frac{\text{mulIndicator}_s f}{\text{mulIndicator}_s g}, \] where $\text{mulIndicator}_s h$ for a function $h \colon \alpha \to G$ is defined as: \[ \text{mulIndicator}_s h (x) = \begin{cases} h(x) & \text{if } x \in s, \\ 1 & \text{otherwise.} \end{cases} \]
Set.mulIndicator_div' theorem
(s : Set α) (f g : α → G) : mulIndicator s (f / g) = mulIndicator s f / mulIndicator s g
Full source 
@[to_additive]
theorem mulIndicator_div' (s : Set α) (f g : α → G) :
    mulIndicator s (f / g) = mulIndicator s f / mulIndicator s g :=
  mulIndicator_div s f g
Multiplicative Indicator Preserves Pointwise Division (Alternative Form)
Informal description
For any set \( s \subseteq \alpha \) and functions \( f, g : \alpha \to G \) (where \( G \) is a group), the multiplicative indicator function of \( s \) applied to the pointwise division \( f / g \) is equal to the pointwise division of the multiplicative indicator functions of \( s \) applied to \( f \) and \( g \). That is: \[ \text{mulIndicator}_s \left( \frac{f}{g} \right) = \frac{\text{mulIndicator}_s f}{\text{mulIndicator}_s g}, \] where the multiplicative indicator function is defined as: \[ \text{mulIndicator}_s h (x) = \begin{cases} h(x) & \text{if } x \in s, \\ 1 & \text{otherwise.} \end{cases} \]
Set.mulIndicator_compl theorem
(s : Set α) (f : α → G) : mulIndicator sᶜ f = f * (mulIndicator s f)⁻¹
Full source 
@[to_additive indicator_compl']
theorem mulIndicator_compl (s : Set α) (f : α → G) :
    mulIndicator sᶜ f = f * (mulIndicator s f)⁻¹ :=
  eq_mul_inv_of_mul_eq <| s.mulIndicator_compl_mul_self f
Complementary Multiplicative Indicator as Product with Inverse
Informal description
For any set $s \subseteq \alpha$ and function $f : \alpha \to G$ (where $G$ is a group), the multiplicative indicator function of the complement $s^c$ satisfies: \[ \text{mulIndicator}_{s^c} f = f \cdot (\text{mulIndicator}_s f)^{-1} \] where $\text{mulIndicator}_s f$ is defined as $f(x)$ if $x \in s$ and $1$ otherwise.
Set.mulIndicator_compl' theorem
(s : Set α) (f : α → G) : mulIndicator sᶜ f = f / mulIndicator s f
Full source 
@[to_additive indicator_compl]
theorem mulIndicator_compl' (s : Set α) (f : α → G) :
    mulIndicator sᶜ f = f / mulIndicator s f := by rw [div_eq_mul_inv, mulIndicator_compl]
Complementary Multiplicative Indicator as Quotient with Indicator
Informal description
For any set $s \subseteq \alpha$ and function $f : \alpha \to G$ (where $G$ is a group), the multiplicative indicator function of the complement $s^c$ satisfies: \[ \text{mulIndicator}_{s^c} f = \frac{f}{\text{mulIndicator}_s f} \] where $\text{mulIndicator}_s f$ is defined as $f(x)$ if $x \in s$ and $1$ otherwise.
Set.mulIndicator_diff theorem
(h : s ⊆ t) (f : α → G) : mulIndicator (t \ s) f = mulIndicator t f * (mulIndicator s f)⁻¹
Full source 
@[to_additive indicator_diff']
theorem mulIndicator_diff (h : s ⊆ t) (f : α → G) :
    mulIndicator (t \ s) f = mulIndicator t f * (mulIndicator s f)⁻¹ :=
  eq_mul_inv_of_mul_eq <| by
    rw [Pi.mul_def, ← mulIndicator_union_of_disjoint, diff_union_self,
      union_eq_self_of_subset_right h]
    exact disjoint_sdiff_self_left
Multiplicative Indicator on Set Difference: $\text{mulIndicator}_{t \setminus s} f = \text{mulIndicator}_t f \cdot (\text{mulIndicator}_s f)^{-1}$
Informal description
For any sets $s \subseteq t \subseteq \alpha$ and any function $f \colon \alpha \to G$ (where $G$ is a group), the multiplicative indicator function on the set difference $t \setminus s$ satisfies: \[ \text{mulIndicator}_{t \setminus s} f = \text{mulIndicator}_t f \cdot (\text{mulIndicator}_s f)^{-1}, \] where $\text{mulIndicator}_S f (x) = f(x)$ if $x \in S$ and $1$ otherwise.
Set.mulIndicator_diff' theorem
(h : s ⊆ t) (f : α → G) : mulIndicator (t \ s) f = mulIndicator t f / mulIndicator s f
Full source 
@[to_additive indicator_diff]
theorem mulIndicator_diff' (h : s ⊆ t) (f : α → G) :
    mulIndicator (t \ s) f = mulIndicator t f / mulIndicator s f := by
  rw [mulIndicator_diff h, div_eq_mul_inv]
Multiplicative Indicator on Set Difference: \(\text{mulIndicator}_{t \setminus s} f = \text{mulIndicator}_t f / \text{mulIndicator}_s f\)
Informal description
For any sets \( s \subseteq t \subseteq \alpha \) and any function \( f \colon \alpha \to G \) (where \( G \) is a group), the multiplicative indicator function on the set difference \( t \setminus s \) satisfies: \[ \text{mulIndicator}_{t \setminus s} f = \frac{\text{mulIndicator}_t f}{\text{mulIndicator}_s f}, \] where \(\text{mulIndicator}_S f (x) = f(x)\) if \( x \in S \) and \( 1 \) otherwise.
Set.apply_mulIndicator_symmDiff theorem
{g : G → β} (hg : ∀ x, g x⁻¹ = g x) (s t : Set α) (f : α → G) (x : α) : g (mulIndicator (s ∆ t) f x) = g (mulIndicator s f x / mulIndicator t f x)
Full source 
@[to_additive]
theorem apply_mulIndicator_symmDiff {g : G → β} (hg : ∀ x, g x⁻¹ = g x)
    (s t : Set α) (f : α → G) (x : α) :
    g (mulIndicator (s ∆ t) f x) = g (mulIndicator s f x / mulIndicator t f x) := by
  by_cases hs : x ∈ s <;> by_cases ht : x ∈ t <;> simp [mem_symmDiff, *]
Symmetric Difference Multiplicative Indicator Property: $g(\text{mulIndicator}_{s \Delta t} f) = g(\text{mulIndicator}_s f / \text{mulIndicator}_t f)$
Informal description
For any function $g \colon G \to \beta$ satisfying $g(x^{-1}) = g(x)$ for all $x \in G$, any sets $s, t \subseteq \alpha$, any function $f \colon \alpha \to G$, and any element $x \in \alpha$, we have: \[ g\left(\text{mulIndicator}_{s \Delta t} f (x)\right) = g\left(\frac{\text{mulIndicator}_s f (x)}{\text{mulIndicator}_t f (x)}\right), \] where $\text{mulIndicator}_s f (x)$ is the multiplicative indicator function of $f$ on $s$ (equal to $f(x)$ if $x \in s$ and $1$ otherwise), and $s \Delta t$ denotes the symmetric difference of $s$ and $t$.
MonoidHom.map_mulIndicator theorem
{M N : Type*} [MulOneClass M] [MulOneClass N] (f : M →* N) (s : Set α) (g : α → M) (x : α) : f (s.mulIndicator g x) = s.mulIndicator (f ∘ g) x
Full source 
@[to_additive]
theorem MonoidHom.map_mulIndicator {M N : Type*} [MulOneClass M] [MulOneClass N] (f : M →* N)
    (s : Set α) (g : α → M) (x : α) : f (s.mulIndicator g x) = s.mulIndicator (f ∘ g) x := by
  simp [Set.mulIndicator_comp_of_one]
Monoid Homomorphism Preserves Multiplicative Indicator Function
Informal description
Let $M$ and $N$ be monoids, and let $f \colon M \to N$ be a monoid homomorphism. For any set $s \subseteq \alpha$ and any function $g \colon \alpha \to M$, the following equality holds for all $x \in \alpha$: \[ f\left(\text{mulIndicator}_s \, g \, x\right) = \text{mulIndicator}_s (f \circ g) \, x, \] where $\text{mulIndicator}_s$ denotes the multiplicative indicator function (which equals $g(x)$ when $x \in s$ and $1$ otherwise).