Set.indicator_union_of_not_mem_inter
theorem Set.indicator_union_of_not_mem_inter :
∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] {s t : Set α} {a : α},
a ∉ s ∩ t → ∀ (f : α → M), (s ∪ t).indicator f a = s.indicator f a + t.indicator f a
The theorem `Set.indicator_union_of_not_mem_inter` states that for any type `α` and `M` where `M` is an additive group, given two sets `s` and `t` of type `Set α`, and an element `a` of type `α`, if the element `a` does not belong to the intersection of the sets `s` and `t`, then for any function `f` from `α` to `M`, the indicator function of the union of the sets `s` and `t` applied to `a` equals the sum of the indicator function of `s` applied to `a` and the indicator function of `t` applied to `a`. In other words, the indicator of a union of two disjoint sets at a point is the sum of the indicators of the sets at that point.
More concisely: If sets `s` and `t` have no common element `a`, then the indicator function of `s ∪ t` at `a` equals the sum of the indicator functions of `s` and `t` at `a`.
|
Set.indicator_zero
theorem Set.indicator_zero :
∀ {α : Type u_1} (M : Type u_4) [inst : Zero M] (s : Set α), (s.indicator fun x => 0) = fun x => 0
This theorem states that for any type `α` and any set `s` of type `Set α`, if we apply the `Set.indicator` function to `s` using a function that maps every element of `α` to '0' (i.e., the zero element of `M`), then we'll always get a function that maps every element of `α` to '0'. In other words, regardless of whether an element is in the set `s` or not, using `Set.indicator` with a constant zero function will always yield a constant zero function.
More concisely: For any set `s` of type `α`, the application of `Set.indicator` to `s` using the constant zero function results in a function equal to the constant zero function.
|
Set.indicator_mul_right
theorem Set.indicator_mul_right :
∀ {α : Type u_1} {M : Type u_4} [inst : MulZeroClass M] {a : α} (s : Set α) (f g : α → M),
s.indicator (fun a => f a * g a) a = f a * s.indicator g a
The theorem `Set.indicator_mul_right` expresses a property of the indicator function on a set with respect to multiplication. Specifically, for any set `s` of a certain type `α` and two functions `f` and `g` from `α` to another type `M` (where `M` is a type with a multiplication operation that has a zero element), the indicator of `s` applied to the product of `f` and `g` at a point `a` equals the product of `f(a)` and the indicator of `s` applied to `g` at `a`. In other words, when we have the product of two functions, we can "move" the indicator function from being applied to the whole product to being applied to just one of the functions.
More concisely: For any set `s` and functions `f` and `g` from a type with a multiplication operation to another type with a zero element, `indicator_of_s (f × g) a = indicator_of_s (g a) × f a`, where `indicator_of_s` denotes the indicator function of `s`.
|
Set.indicator_of_mem
theorem Set.indicator_of_mem :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Set α} {a : α}, a ∈ s → ∀ (f : α → M), s.indicator f a = f a
The theorem `Set.indicator_of_mem` asserts that for any type `α`, type `M` equipped with a zero element, a set `s` of elements of type `α`, and an element `a` of type `α`, if `a` is an element of the set `s`, then the indicator function of the set `s` applied to the function `f` and the element `a` equals the function `f` applied to the element `a`. In other words, if `a` belongs to `s`, the set indicator will simply return the value of function `f` at `a`. This theorem essentially defines the behavior of the set indicator function when the element is within the set.
More concisely: For any set `s` of type `α` and function `f` from `α` to a type `B`, if `a` is an element of `s`, then `indicator_s a = f a`.
|
Set.indicator_of_not_mem
theorem Set.indicator_of_not_mem :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Set α} {a : α}, a ∉ s → ∀ (f : α → M), s.indicator f a = 0
The theorem `Set.indicator_of_not_mem` states that for any set `s` of elements of type `α`, any function `f` from `α` to `M` and any element `a` of type `α`, if `a` is not a member of `set s`, then the set indicator of `s`, `f`, and `a` equals `0`. Here, the set indicator of `s`, `f`, and `a` is defined as `f a` if `a` is in the set `s` and `0` otherwise. In other words, the theorem expresses that if an element does not belong to a specific set, the set indicator function for that element and set returns zero. This is a property of the set indicator function in the context of mathematical set theory.
More concisely: For any set `s` of type `α`, any function `f : α → M`, and any `a : α`, if `a` is not in `s`, then `f a = 0`.
|
Set.indicator_union_of_disjoint
theorem Set.indicator_union_of_disjoint :
∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] {s t : Set α},
Disjoint s t → ∀ (f : α → M), (s ∪ t).indicator f = fun a => s.indicator f a + t.indicator f a
The theorem `Set.indicator_union_of_disjoint` states that for any two disjoint sets `s` and `t` of any type `α`, and for any function `f` from `α` to a type `M` which has addition and zero, the indicator function of the union of `s` and `t` with respect to `f` is the sum of the indicator functions of `s` and `t` with respect to `f`. Here, the indicator function of a set `s` is a function that takes an element `a` and maps it to `f(a)` if `a` belongs to `s`, and to zero otherwise. Two sets are considered disjoint if they have no element in common.
More concisely: For any disjoint sets `s` and `t` of type `α` and any function `f` from `α` to a type `M` with addition and zero, the indicator function of `s ∪ t` with respect to `f` equals the sum of the indicator functions of `s` and `t` with respect to `f`.
|
Set.indicator_support
theorem Set.indicator_support :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f : α → M}, (Function.support f).indicator f = f
This theorem states that, given a function `f` from some type `α` to another type `M` where `M` has a zero element, the `Set.indicator` of the `Function.support` of `f` and `f` itself is equal to `f`. In other words, if we create a function that takes a value from `f` when the input is in the support of `f` (the set of points where `f` does not return zero) and returns zero otherwise, we end up with the original function `f`.
More concisely: Given a function `f` from type `α` to type `M` with `M` having a zero element, `Function.support f`'s indicator function equals `f`.
|
Set.mem_of_indicator_ne_zero
theorem Set.mem_of_indicator_ne_zero :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Set α} {f : α → M} {a : α}, s.indicator f a ≠ 0 → a ∈ s := by
sorry
The theorem `Set.mem_of_indicator_ne_zero` states that for any types `α` and `M`, where `M` has a zero element, given a set `s` of type `α`, a function `f` from `α` to `M`, and an element `a` of type `α`, if the additive indicator function of `s` at `a` under `f` is not zero, then `a` is an element of the set `s`. Essentially, this theorem connects the non-zero value of an additive indicator function at a point to the membership of that point in the respective set.
More concisely: If the additive indicator function of a set with respect to a function is not zero at an element, then that element is in the set.
|
Set.indicator_apply
theorem Set.indicator_apply :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (s : Set α) (f : α → M) (a : α) [inst_1 : Decidable (a ∈ s)],
s.indicator f a = if a ∈ s then f a else 0
The theorem `Set.indicator_apply` states that for any set `s` of some type `α`, a function `f` from `α` to another type `M` that has a zero element (denoted by `[Zero M]`), and an element `a` of type `α`, if it is decidable whether `a` belongs to the set `s` (denoted by `[Decidable (a ∈ s)]`), then applying the `Set.indicator` function on `s`, `f`, and `a` yields the same result as checking whether `a` belongs to `s`: if `a` does belong, it returns the result of applying `f` on `a`; if `a` does not belong, it returns the zero element of `M`.
More concisely: If `s` is a set of type `α` with a decidable membership relation and `f: α → M` is a function with a zero element, then `Set.indicator s f` is the characteristic function of `s` with respect to `f`.
|
Set.mulIndicator_of_not_mem
theorem Set.mulIndicator_of_not_mem :
∀ {α : Type u_1} {M : Type u_4} [inst : One M] {s : Set α} {a : α}, a ∉ s → ∀ (f : α → M), s.mulIndicator f a = 1
The theorem `Set.mulIndicator_of_not_mem` states that for any types `α` and `M`, where `M` has the structure of a monoid (given by the instance `One M`), any set `s` of type `α`, and any element `a` of type `α`, if `a` is not an element of the set `s`, then for any function `f` mapping elements of `α` to `M`, the multiplicative indicator function of the set `s` evaluated at `a` with respect to the function `f` is equal to the multiplicative identity in `M`, which is `1`. In other words, when an element does not belong to a particular set, the multiplicative indicator function for that set returns `1` irrespective of the function `f`.
More concisely: For any monoid `M`, set `s` of type `α`, and element `a` not in `s`, the multiplicative indicator function `Set.mulIndicator s f` of `s` with respect to a function `f` mapping elements of `α` to `M` equals the multiplicative identity `1` in `M`.
|
Set.mulIndicator_one
theorem Set.mulIndicator_one :
∀ {α : Type u_1} (M : Type u_4) [inst : One M] (s : Set α), (s.mulIndicator fun x => 1) = fun x => 1
The theorem `Set.mulIndicator_one` states that for any type `α`, for any Monoid `M` with an identity element `1`, and for any set `s` of type `α`, the multiplication indicator of the set `s` with the constant function that always returns `1` is equal to the constant function that always returns `1`. In other words, regardless of whether an element is in set `s` or not, the multiplication indicator will always output `1`.
More concisely: For any set `s` and monoid `M` with identity `1`, the multiplication indicator of `s` with the constant function mapping to `1` equals the constant function mapping to `1`. In Lean, this is expressed as `Set.mulIndicator s (λ _ => 1) = λ _ => 1`.
|
Set.indicator_eq_one_iff_mem
theorem Set.indicator_eq_one_iff_mem :
∀ {α : Type u_1} (M : Type u_4) [inst : MulZeroOneClass M] [inst_1 : Nontrivial M] {U : Set α} {x : α},
U.indicator 1 x = 1 ↔ x ∈ U
The theorem `Set.indicator_eq_one_iff_mem` states that for any type `α` and a multiplicative monoid with zero and one `M` (which is nontrivial), given a set `U` of type `α` and an element `x` of type `α`, the set indicator function of `U` evaluated at `x` with function value `1` is equal to `1` if and only if `x` is an element of the set `U`. In other words, within this mathematical structure, an element `x` belongs to a set `U` precisely when its set indicator with a constant function of `1` returns `1`.
More concisely: For any set U of type α and multiplicative monoid M with zero and one, the indicator function iU of U evaluated at x equals 1 if and only if x is a member of U.
|
Set.piecewise_eq_indicator
theorem Set.piecewise_eq_indicator :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Set α} {f : α → M} [inst_1 : DecidablePred fun x => x ∈ s],
s.piecewise f 0 = s.indicator f
This theorem states that for any type `α`, any type `M` equipped with a zero element, any set `s` of `α`, and any function `f` from `α` to `M`, the piecewise function on `s` that is equal to `f` on `s` and zero elsewhere is the same as the indicator function of `s` with respect to `f`. This holds if the predicate "an element belongs to `s`" is decidable. In mathematical terms, if `f : α → M` and `s` is a subset of `α`, then the function `s.piecewise f 0` equals the function `Set.indicator s f`, where `Set.indicator s f a` equals `f(a)` if `a` is in `s` and `0` otherwise.
More concisely: For any type `α`, set `s` of `α` with decidable membership, and function `f : α → M`, the piecewise function `s.piecewise f 0` equals the indicator function `Set.indicator s f`.
|
Set.mulIndicator_union_of_not_mem_inter
theorem Set.mulIndicator_union_of_not_mem_inter :
∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] {s t : Set α} {a : α},
a ∉ s ∩ t → ∀ (f : α → M), (s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
The theorem `Set.mulIndicator_union_of_not_mem_inter` states that for any types `α` and `M`, given a multiplication and one identity structure on `M`, any two sets `s` and `t` of type `α`, and any element `a` of type `α` that is not in the intersection of `s` and `t`, for any function `f` from `α` to `M`, the multiplicative indicator function of the union of `s` and `t` applied to `f` at `a` is equal to the product of the multiplicative indicator function of `s` applied to `f` at `a` and the multiplicative indicator function of `t` applied to `f` at `a`. In simpler terms, if an element does not belong to the intersection of two sets, the value of the multiplicative indicator function at this element for the union of the sets is the product of the values of the multiplicative indicator function for the individual sets.
More concisely: For sets `s` and `t` of type `α` and for any element `a ∉ s ∩ t` of type `α`, the multiplicative indicator function of `s ∪ t` at `f(a)` is equal to the product of the multiplicative indicator functions of `s` and `t` at `f(a)`.
|
Set.support_indicator
theorem Set.support_indicator :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Set α} {f : α → M},
Function.support (s.indicator f) = s ∩ Function.support f
This theorem states that for any given types `α` and `M`, with `M` having a zero element, any set `s` of type `α`, and function `f` from `α` to `M`, the support of the indicator function of `s` and `f` is the intersection of `s` and the support of `f`. In other words, the support of the indicator function, which is the set of points where the indicator function is not zero, is precisely the set of points that are in both `s` and the locations where `f` is not zero.
More concisely: The support of the indicator function of a set `s` and a function `f` from `α` to a type `M` with a zero element is equal to the intersection of `s` and the support of `f`.
|
Set.mulIndicator_preimage
theorem Set.mulIndicator_preimage :
∀ {α : Type u_1} {M : Type u_4} [inst : One M] (s : Set α) (f : α → M) (B : Set M),
s.mulIndicator f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B)
This theorem states that for all types `α` and `M`, with `M` being a type that has a multiplicative identity (`One M`), a set `s` of type `α`, a function `f` from `α` to `M`, and a set `B` of type `M`, the preimage of `B` under the function `Set.mulIndicator s f` (which is a function that returns `f a` if `a` is in `s` and `1` otherwise) is equivalent to a set which is the union of the intersection of the preimage of `B` under `f` and `s`, and the set difference of the preimage of `B` under the singleton set `{1}` and `s`. This means, the elements in `α` that get mapped to `B` when using the `Set.mulIndicator s f` function are those that either belong to `s` and get mapped to `B` when using the original function `f`, or don't belong to `s` and get mapped to `1`.
More concisely: For all types `α` and `M` with a multiplicative identity, and functions `f: α -> M` and `s: Set α`, the sets `{x : α | Set.mulIndicator s f x ∈ B}` and `(s ∩ {x : α | f x ∈ B}) ∪ ({1} \ s)` are equal.
|
Mathlib.Algebra.Function.Indicator._auxLemma.9
theorem Mathlib.Algebra.Function.Indicator._auxLemma.9 :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Set α} {f : α → M} {a : α},
(s.indicator f a = 0) = (a ∈ s → f a = 0)
This theorem states that for any set `s` of elements of type `α`, any function `f` from `α` to `M`, and any element `a` of type `α`, the indicator function of `s` applied to `f` and `a` is equal to `0` if and only if the element `a` is in the set `s` and the function `f` applied to `a` equals `0`. In mathematical terms, we have $\text{Set.indicator } s f a = 0$ if and only if $a \in s \rightarrow f(a) = 0$ for any types `α` and `M` with `M` having a zero element.
More concisely: For any set `s` of type `α`, function `f` from `α` to a type `M` with zero element, and element `a` of type `α`, the indicator function of `s` applied to `f` and `a` equals `0` if and only if `a` is in `s` and `f(a)` equals `0`.
|
Set.support_indicator_subset
theorem Set.support_indicator_subset :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Set α} {f : α → M}, Function.support (s.indicator f) ⊆ s := by
sorry
The theorem `Set.support_indicator_subset` asserts that for any type `α`, any type `M` with a zero element, any set `s` of elements of type `α`, and any function `f` from `α` to `M`, the support of the set indicator function of `s` and `f` is a subset of `s`. In other words, the set of all points `x` in `α` where the function `Set.indicator s f` does not equal zero, is contained within `s`. Here, `Set.indicator s f` is a function that gives the value `f(x)` for `x` in `s`, and zero otherwise.
More concisely: For any set `s` in type `α` and any function `f` from `α` to a type `M` with a zero element, the set where `Set.indicator s f` is non-zero is contained in `s`.
|
Set.indicator_add
theorem Set.indicator_add :
∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] (s : Set α) (f g : α → M),
(s.indicator fun a => f a + g a) = fun a => s.indicator f a + s.indicator g a
The theorem `Set.indicator_add` states that for any set `s` of elements of a certain type `α` and any two functions `f` and `g` from `α` to another type `M` (where `M` is a type with an addition operation and a zero element), the indicator function of `s` applied to the sum of `f` and `g` at a point `a` is equal to the sum of the indicator functions of `s` applied to `f` and `g` respectively at `a`. In mathematical terms, this can be written as: for all `a` in `α`, `Set.indicator s (f(a) + g(a)) = Set.indicator s f(a) + Set.indicator s g(a)`. This theorem essentially distributes the indicator function over the addition of the two functions.
More concisely: For any set `s` and functions `f` and `g` from a type `α` to a type `M` with addition, the indicator function of `s` applied to the sum of `f` and `g` equals the sum of the indicator functions of `s` applied to `f` and `g`: `Set.indicator s (f + g) = Set.indicator s f + Set.indicator s g`.
|
Set.mulIndicator_of_mem
theorem Set.mulIndicator_of_mem :
∀ {α : Type u_1} {M : Type u_4} [inst : One M] {s : Set α} {a : α},
a ∈ s → ∀ (f : α → M), s.mulIndicator f a = f a
This theorem states that for any types `α` and `M`, where `M` is a type with a defined `One` instance, any set `s` of type `α`, and any element `a` of type `α`, if `a` is an element of `s`, then the result of the `mulIndicator` function applied to `s`, a function `f` from `α` to `M`, and `a` is simply `f(a)`. In other words, when `a` belongs to the `s` set, `Set.mulIndicator s f a` is equal to `f a`.
More concisely: For any set `s` of type `α`, function `f` from `α` to a type `M` with a defined `One` instance, if `a` is an element of `s`, then `Set.mulIndicator s f a = f a`.
|
Set.mulIndicator_mulSupport
theorem Set.mulIndicator_mulSupport :
∀ {α : Type u_1} {M : Type u_4} [inst : One M] {f : α → M}, (Function.mulSupport f).mulIndicator f = f
The theorem `Set.mulIndicator_mulSupport` states that for any type `α`, any type `M` equipped with a multiplicative identity element, and any function `f` from `α` to `M`, the function obtained by applying the `Set.mulIndicator` operation to the `Function.mulSupport` of `f` and `f` itself is equivalent to `f`. In other words, when we restrict `f` to the set of points where `f` is not equal to the multiplicative identity (the `Function.mulSupport` of `f`), and define this restricted function to return `f x` for `x` in this set and `1` otherwise (the `Set.mulIndicator` operation), we get back the original function `f`.
More concisely: For any type `α` and any function `f` from `α` to a type `M` with multiplicative identity, the restricted function obtained by applying `Set.mulIndicator` to the support of `f` is equal to `f` itself.
|
Set.indicator_comp_of_zero
theorem Set.indicator_comp_of_zero :
∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] {s : Set α} {f : α → M}
{g : M → N}, g 0 = 0 → s.indicator (g ∘ f) = g ∘ s.indicator f
The theorem `Set.indicator_comp_of_zero` states that for any set `s` of elements of type `α`, any function `f` mapping elements of type `α` to type `M`, and any function `g` mapping elements of type `M` to type `N` (given that zero of both types `M` and `N` are defined and the function `g` maps `0` to `0`), the indicator function of the composition `g ∘ f` on the set `s` is equal to the composition of `g` and the indicator function of `f` on the set `s`. In other words, the indicator function commutes with the composition of functions whenever the second function sends `0` to `0`.
More concisely: For any set `s` and functions `f: α → M`, `g: M → N` with `0` defined in types `M` and `N` and `g(0) = 0`, the indicator functions of `g ∘ f` and `g ∘ Indicator_fun s ∘ f` on set `s` are equal.
|
Mathlib.Algebra.Function.Indicator._auxAddLemma.4
theorem Mathlib.Algebra.Function.Indicator._auxAddLemma.4 :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α → M} {x : α}, (x ∈ Function.support f) = (f x ≠ 0) := by
sorry
This theorem, named `Mathlib.Algebra.Function.Indicator._auxAddLemma.4`, states that for any type `α` and `M` where `M` is a type with a zero element, and given any function `f` from `α` to `M` and any element `x` of type `α`, the statement "x is in the support of f" is equivalent to "the value of function f at x is not equal to zero". Here, the `support` of a function is defined as the set of points `x` such that `f(x) ≠ 0`.
More concisely: For any type `α` and `M` with a zero element, and any function `f` from `α` to `M`, the element `x` is in the support of `f` if and only if `f(x) ≠ 0`.
|
Set.indicator_preimage
theorem Set.indicator_preimage :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (s : Set α) (f : α → M) (B : Set M),
s.indicator f ⁻¹' B = s.ite (f ⁻¹' B) (0 ⁻¹' B)
This theorem states that, for any set `s` of elements of type `α`, any function `f` from `α` to `M` where `M` is a type with a zero element, and any set `B` of elements of type `M`, the preimage of `B` under the "indicator function" of `s` and `f` is equal to the `ite` (if-then-else) of `s`, the preimage of `B` under `f`, and the preimage of `B` under constant zero function. In other words, if you first apply the indicator function to `s` and `f` and then take the preimage of `B`, it's the same as if you first take the preimage of `B` under `f` and the constant zero function, then take the `ite` of these with respect to `s`.
More concisely: For any set `s` of elements of type `α`, function `f` from `α` to a type `M` with zero element, and set `B` of elements of type `M`, the indicator function of `s` and `f`'s preimage of `B` equals the `ite` of `s`, `f`'s preimage of `B`, and the preimage of `B` under the constant zero function.
|
Set.mulIndicator_eq_self
theorem Set.mulIndicator_eq_self :
∀ {α : Type u_1} {M : Type u_4} [inst : One M] {s : Set α} {f : α → M},
s.mulIndicator f = f ↔ Function.mulSupport f ⊆ s
This theorem states that for any set `s` of type `α` and a function `f` from `α` to some type `M` equipped with a distinguished "one" element, the "multiplicative indicator function" of `s` and `f` is equal to `f` if and only if the "multiplicative support" of `f` is a subset of `s`. In mathematical terms, the "multiplicative indicator function" `Set.mulIndicator s f a` is defined to be `f(a)` if `a` is in `s`, and `1` otherwise. The "multiplicative support" `Function.mulSupport f` of a function `f` is the set of all points `x` such that `f(x)` is not equal to `1`. Hence, this theorem links the equality of a function to its multiplicative indicator function with the containment of its multiplicative support within a certain set.
More concisely: For any set `s` and function `f` from type `α` to a type with a distinguished "one" element, the multiplicative indicator function of `s` and `f` equals `f` if and only if the multiplicative support of `f` is contained in `s`.
|
Set.mulIndicator_eq_one
theorem Set.mulIndicator_eq_one :
∀ {α : Type u_1} {M : Type u_4} [inst : One M] {s : Set α} {f : α → M},
(s.mulIndicator f = fun x => 1) ↔ Disjoint (Function.mulSupport f) s
This theorem states that for any set `s` of type `α` and any function `f` from `α` to `M` where `M` is a type with an identity element, the "multiplicative indicator function" of `s` and `f` is equal to the constant function returning the identity element if and only if the "multiplicative support" of `f` (the set of points `x` where `f(x)` is not the identity) is disjoint from `s`. Here, two sets are considered disjoint if their infimum is the "bottom" element, which in this context means that there is no element that is in both sets.
More concisely: For any set `s` of type `α` and function `f` from `α` to a type `M` with an identity element, the multiplicative indicator function of `s` and `f` equals the constant function returning the identity element if and only if the support of `f` and `s` are disjoint.
|
Set.mem_of_mulIndicator_ne_one
theorem Set.mem_of_mulIndicator_ne_one :
∀ {α : Type u_1} {M : Type u_4} [inst : One M] {s : Set α} {f : α → M} {a : α}, s.mulIndicator f a ≠ 1 → a ∈ s := by
sorry
This theorem states that for any type `α` and `M`, if `M` is equipped with a multiplicative identity (`1`), and given any set `s` of type `α`, any function `f` from `α` to `M`, and any element `a` of type `α`, if the multiplicative indicator function of the set `s` with respect to the function `f` evaluated at `a` is not equal to `1`, then `a` is an element of the set `s`. This means "not equal to `1`" is an indicator of membership in the set `s` under the function `f`.
More concisely: If `M` is a type with a multiplicative identity, `s` is a set of type `α`, `f : α → M`, and `1 ≠ f a` for some `a : α`, then `a ∈ s`.
|
Set.indicator_univ
theorem Set.indicator_univ : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (f : α → M), Set.univ.indicator f = f := by
sorry
The theorem `Set.indicator_univ` states that for any set `α` and any type `M` equipped with a zero element (`inst : Zero M`), and any function `f` from `α` to `M`, applying the Set.indicator function to the universal set and `f` will just yield `f`. In simpler terms, if we use the indicator function with the universal set, it does not change the function `f` because the indicator only applies function `f` when an element is in the set, and all elements are in the universal set.
More concisely: For any set α and type M with a zero element, the indicator function of the universal set and a function from α to M are equal.
|
AddMonoidHom.map_indicator
theorem AddMonoidHom.map_indicator :
∀ {α : Type u_1} {M : Type u_6} {N : Type u_7} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N)
(s : Set α) (g : α → M) (x : α), f (s.indicator g x) = s.indicator (⇑f ∘ g) x
The theorem `AddMonoidHom.map_indicator` states that for any types `α`, `M`, and `N` where `M` and `N` are additive monoids (having an addition operation and a zero element), for any additive monoid homomorphism `f` from `M` to `N`, any set `s` of type `α`, any function `g` from `α` to `M`, and any element `x` of type `α`, the value of `f` applied to the indicator function of `s` and `g` at `x` equals the indicator function of `s` and `f` composed with `g` at `x`.
In other words, if you have an additive monoid homomorphism and you apply it to the indicator function of a set, it's the same as if you first applied the function to the elements of the set and then calculated the indicator function. It essentially states that the process of applying the homomorphism commutes with the process of calculating the indicator function.
More concisely: For any additive monoid homomorphism between additive monoids `M` and `N`, and any set `s` with indicator function `ind_s` and function `g` from `α` to `M`, `f(ind_s(g))(x) = ind_s(f(g(x)))` for all `x` in `α`.
|
Set.apply_indicator_symmDiff
theorem Set.apply_indicator_symmDiff :
∀ {α : Type u_1} {β : Type u_2} {G : Type u_6} [inst : AddGroup G] {g : G → β},
(∀ (x : G), g (-x) = g x) →
∀ (s t : Set α) (f : α → G) (x : α), g ((symmDiff s t).indicator f x) = g (s.indicator f x - t.indicator f x)
This theorem, named `Set.apply_indicator_symmDiff`, states that for any types `α`, `β` and `G` with `G` being an additive group, and any function `g` from `G` to `β` satisfying the property `g (-x) = g x` for all `x` in `G`, and for any sets `s` and `t` of type `α` with a function `f` from `α` to `G`, the application of `g` to the set indicator of the symmetric difference of `s` and `t` at any point `x` is equal to the application of `g` to the difference of the set indicators of `s` and `t` at `x`.
In simpler terms, it says that for a suitable function `g` and any sets `s` and `t`, the value of `g` at the `Set.indicator` of the symmetric difference of `s` and `t` is the same as the value of `g` at the difference of the `Set.indicator`s of `s` and `t`. This holds true for any point `x` in the sets.
More concisely: For any additive group G, functions g from G to a type β satisfying g (-x) = g x for all x in G, and sets s and t, the application of g to the set indicator of the symmetric difference of s and t is equal to the application of g to the difference of the set indicators of s and t at any point x in the sets.
|
Set.mulSupport_mulIndicator
theorem Set.mulSupport_mulIndicator :
∀ {α : Type u_1} {M : Type u_4} [inst : One M] {s : Set α} {f : α → M},
Function.mulSupport (s.mulIndicator f) = s ∩ Function.mulSupport f
The theorem `Set.mulSupport_mulIndicator` states that for any set `s` of type `α` and any function `f` from `α` to `M` where `M` has a defined "one" element, the multiplicative support of the function defined by the multiplicative indicator of `s` and `f` is equivalent to the intersection of `s` and the multiplicative support of `f`. In other words, the set of points `x` where the multiplicative indicator function does not equal "one" is the same as the set of points `x` that are both in `s` and where `f(x)` does not equal "one".
More concisely: The multiplicative support of the multiplicative indicator function of a set and a function is equal to the intersection of that set and the support of the function.
|
Set.indicator_eq_zero
theorem Set.indicator_eq_zero :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Set α} {f : α → M},
(s.indicator f = fun x => 0) ↔ Disjoint (Function.support f) s
The theorem `Set.indicator_eq_zero` states that for any set `s` of elements of type `α`, and any function `f` from `α` to any Type `M` with a defined `Zero`, the indicator function `Set.indicator s f` is identically zero if and only if the support of `f`, i.e., the set of points `x` where `f(x)` is not zero, is disjoint from the set `s`. Here, two elements (or sets) are defined to be disjoint if their infimum (greatest lower bound) is the bottom element of the lattice.
More concisely: The indicator function of a set with respect to a function is equal to the zero function if and only if the support of the function is disjoint from the set.
|
Mathlib.Algebra.Function.Indicator._auxLemma.8
theorem Mathlib.Algebra.Function.Indicator._auxLemma.8 :
∀ {α : Type u_1} {M : Type u_4} [inst : One M] {s : Set α} {f : α → M} {a : α},
(s.mulIndicator f a = 1) = (a ∈ s → f a = 1)
This theorem states that for any set `s` of type `α` and any function `f : α → M`, where `M` is a type with an identity element `1`, the `Set.mulIndicator` of `s`, `f`, and a particular element `a` of `α` equals `1` if and only if `a` is an element of `s` and the function `f` applied to `a` equals `1`. In other words, the `Set.mulIndicator` returns `1` when `a` is in `s` and `f(a)` is `1`, and otherwise it returns the value of `f` at `a`.
More concisely: For any set `s` of type `α` and function `f : α → M` with `M` having an identity element `1`, `Set.mulIndicator s f a = 1` if and only if `a` is in `s` and `f a = 1`.
|
Set.indicator_zero'
theorem Set.indicator_zero' : ∀ {α : Type u_1} (M : Type u_4) [inst : Zero M] {s : Set α}, s.indicator 0 = 0
The theorem `Set.indicator_zero'` states that for any type `α`, any type `M` that has a zero element (denoted by `[inst : Zero M]`), and any set `s` of type `Set α`, the indicator function of the set `s` with the constant zero function (i.e., `Set.indicator s 0`) is identically zero. In other words, regardless of whether an element is in the set `s` or not, the indicator function will always yield zero when combined with the constant zero function.
More concisely: For any set `s` and type `α` with a zero element, the indicator function of `s` equals the constant zero function. That is, `Set.indicator s 0 = λ x : α, 0`.
|
Set.indicator_empty
theorem Set.indicator_empty : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (f : α → M), ∅.indicator f = fun x => 0
The theorem `Set.indicator_empty` states that for any function `f` mapping elements from an arbitrary type `α` to another type `M` that has a zero element, the set indicator of the empty set and `f` is equivalent to a function that always yields zero. In other words, applying the function `f` over an empty set via a set indicator always results in a zero. This makes sense, since the set indicator is defined to return the result of the function `f` applied to an element if that element is in the set, and zero otherwise. Since the empty set contains no elements, the function `f` can never be applied, and so zero is always returned.
More concisely: For any function `f` from type `α` to a type `M` with a zero element, the set indicator of the empty set and `f` equals the constant function that maps to the zero element of `M`.
|
Mathlib.Algebra.Function.Indicator._auxLemma.4
theorem Mathlib.Algebra.Function.Indicator._auxLemma.4 :
∀ {α : Type u_1} {M : Type u_5} [inst : One M] {f : α → M} {x : α}, (x ∈ Function.mulSupport f) = (f x ≠ 1) := by
sorry
This theorem states that for any type `α` and `M`, where `M` is a type with a specified multiplicative identity, and any function `f` from `α` to `M`, along with any element `x` of type `α`, the element `x` belongs to the `mulSupport` of the function `f` if and only if the value of function `f` at `x` is not equal to the multiplicative identity, which is `1`. In other words, the `mulSupport` of a function `f` is precisely the set of points `x` where `f(x)` is different from the identity element `1`.
More concisely: For any type `α` and `M` with multiplicative identity, and any function `f` from `α` to `M`, the element `x` in `α` is in the `mulSupport` of `f` if and only if `f(x) ≠ 1`.
|
Set.indicator_eq_self
theorem Set.indicator_eq_self :
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Set α} {f : α → M},
s.indicator f = f ↔ Function.support f ⊆ s
The theorem `Set.indicator_eq_self` states that for any type α, any type M with a zero element, any set s of elements of type α, and any function f from α to M, the indicator function for the set s and function f is equal to the function f itself if and only if the support of the function f is a subset of the set s. Here, the support of a function is the set of all points where the function does not output zero, and the indicator function for a set s and a function f outputs the application of the function to an input if the input is in the set and zero otherwise.
More concisely: The indicator function of a set with respect to a function equals the function itself if and only if the function's support is contained in the set.
|