Mathlib.Algebra.Function.Support._auxLemma.1
theorem Mathlib.Algebra.Function.Support._auxLemma.1 :
∀ {α : 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 `α`, a type `M` that has the structure of a `One` (which means it has a specified element considered as "one"), a function `f` from `α` to `M`, and an element `x` of type `α`, the element `x` is in the multiplicative support of the function `f` if and only if the value of `f` at `x` is not equal to `1`. The multiplicative support of the function `f` is defined as the set of points `x` in `α` such that `f(x)` is not `1`.
More concisely: For any type `α`, function `f` from `α` to a One `M`, and `x` in `α`, `x` is in the multiplicative support of `f` if and only if `f(x) ≠ 1`.
|
Function.mulSupport_binop_subset
theorem Function.mulSupport_binop_subset :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst : One M] [inst_1 : One N] [inst_2 : One P]
(op : M → N → P),
op 1 1 = 1 →
∀ (f : α → M) (g : α → N),
(Function.mulSupport fun x => op (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g
This theorem states that for any types `α`, `M`, `N`, and `P`, (where `M`, `N`, and `P` are types with a defined `One` operation), and a binary operation `op` from `M` and `N` to `P` that preserves the `One` operation (i.e., `op 1 1 = 1`), for any functions `f : α → M` and `g : α → N`, the support of the function `x => op (f x) (g x)` (which is the set of points `x` where this function does not return `1`) is a subset of the union of the supports of `f` and `g`. In other words, if the combined function `op (f x) (g x)` does not return `1` for some `x`, then either `f` or `g` (or both) must not return `1` for that `x`.
More concisely: For functions `f : α → M` and `g : α → N` with types `M` and `N` having defined `One` operations, and a binary operation `op` from `M` and `N` to `P` preserving the `One` operation, the support of the function `x => op (f x) (g x)` is a subset of the union of the supports of `f` and `g`.
|
Pi.support_single_of_ne
theorem Pi.support_single_of_ne :
∀ {A : Type u_1} {B : Type u_2} [inst : DecidableEq A] [inst_1 : Zero B] {a : A} {b : B},
b ≠ 0 → Function.support (Pi.single a b) = {a}
The theorem `Pi.support_single_of_ne` states that for any types A and B, given a decidable equality on A and a zero element on B, for any elements 'a' from A and 'b' from B, if 'b' is not zero, then the set of points where the function `Pi.single` (which maps A to B) is not zero is just the singleton set containing 'a'. In other words, the function `Pi.single a b` is only non-zero (i.e., not equal to the zero element of B) at 'a'.
More concisely: Given types A and B with a decidable equality, a zero element in B, and for all a in A and b in B with b not equal to the zero element, `Pi.single a b` is a function equal to `a` as a map from A to B.
|
Function.support_add
theorem Function.support_add :
∀ {α : Type u_1} {M : Type u_5} [inst : AddZeroClass M] (f g : α → M),
(Function.support fun x => f x + g x) ⊆ Function.support f ∪ Function.support g
The theorem `Function.support_add` is stating that for any types `α` and `M`, where `M` is an `AddZeroClass` (meaning it supports addition and has a zero element), and for any two functions `f` and `g` from `α` to `M`, the support of the function that adds `f` and `g` is a subset of the union of the supports of `f` and `g`. In other words, any point `x` for which `f(x) + g(x)` is non-zero must be a point at which either `f(x)` is non-zero, `g(x)` is non-zero, or both.
More concisely: For functions `f` and `g` from type `α` to an additive zero class `M`, `support (f + g) ⊆ support f ∪ support g`.
|
Function.nmem_mulSupport
theorem Function.nmem_mulSupport :
∀ {α : Type u_1} {M : Type u_5} [inst : One M] {f : α → M} {x : α}, x ∉ Function.mulSupport f ↔ f x = 1
The theorem `Function.nmem_mulSupport` states that for any types `α` and `M`, given a function `f` of type `α` to `M`, and an element `x` of type `α`, `x` is not in the `mulSupport` of `f` if and only if the function `f` applied to `x` equals `1`. In other words, a point `x` does not belong to the set of points where `f(x)` is not equal to `1` (the `mulSupport` of `f`) if and only if `f(x) = 1`.
More concisely: For any function `f` from type `α` to `M`, `x` is not in the support of the multiplication action of `f` if and only if `f(x) = 1`.
|
Function.mem_mulSupport
theorem Function.mem_mulSupport :
∀ {α : Type u_1} {M : Type u_5} [inst : One M] {f : α → M} {x : α}, x ∈ Function.mulSupport f ↔ f x ≠ 1
The theorem `Function.mem_mulSupport` states that for any types `α` and `M` (with `M` having an identity element under multiplication), a function `f` from `α` to `M`, and an element `x` of type `α`, `x` is in the `mulSupport` of `f` if and only if the value of `f` at `x` is not equal to the identity element of `M`. In other words, the `mulSupport` of a function `f` is the set of all points `x` where `f(x)` does not equal the multiplicative identity.
More concisely: The theorem `Function.mem_mulSupport` asserts that an element `x` is in the domain of a multiplication function `f` from type `α` to type `M` if and only if `f x` is not the identity element of `M`.
|
Function.mulSupport_one'
theorem Function.mulSupport_one' : ∀ {α : Type u_1} {M : Type u_5} [inst : One M], Function.mulSupport 1 = ∅
The theorem `Function.mulSupport_one'` states that for all types `α` and `M`, with `M` being equipped with an instance of `One` (a structure with a default element usually representing 'one' in some sense), the `mulSupport` of the function that constantly returns one is an empty set. In mathematical terms, it says that for any types `α` and `M` with `M` having a defined 'one', there are no elements in `α` for which the constant function 1 returns a value different from 'one'. Thus, the set of such elements, `mulSupport 1`, is empty.
More concisely: For all types `α` and `M` with a `One` instance, the set of elements `x` in `α` such that the constant function `λ (x : α), 1` does not equal `1` is empty.
|
Function.support_comp_eq_preimage
theorem Function.support_comp_eq_preimage :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (g : β → M) (f : α → β),
Function.support (g ∘ f) = f ⁻¹' Function.support g
The theorem `Function.support_comp_eq_preimage` states that for any types `α`, `β`, and `M` with `M` having a zero element, and for any functions `g : β → M` and `f : α → β`, the support of the composition function `(g ∘ f)` is equal to the preimage of the support of `g` under `f`. In other words, the set of `α` points at which `(g ∘ f)` is non-zero is exactly the set of `α` points whose `f` image is a point where `g` is non-zero.
More concisely: The support of the composition of functions `g ∘ f` from `α` to `M` equals the preimage of the support of `g` under `f`.
|
Pi.support_single_subset
theorem Pi.support_single_subset :
∀ {A : Type u_1} {B : Type u_2} [inst : DecidableEq A] [inst_1 : Zero B] {a : A} {b : B},
Function.support (Pi.single a b) ⊆ {a}
The `Pi.support_single_subset` theorem states that for any types `A` and `B`, where `A` has decidable equality and `B` has a zero element, and any elements `a` of type `A` and `b` of type `B`, the support of the function `Pi.single a b` (which is the function that equals `b` at `a` and zero elsewhere) is a subset of the set containing only `a`. In other words, the only point where `Pi.single a b` is non-zero is at `a`.
More concisely: The support of `Pi.single a b` in Lean, where `A` has decidable equality and `B` has a zero element, is the singleton set `{a}`.
|
Function.support_neg
theorem Function.support_neg :
∀ {α : Type u_1} {G : Type u_10} [inst : SubtractionMonoid G] (f : α → G),
(Function.support fun x => -f x) = Function.support f
The theorem `Function.support_neg` states that for every function `f` mapping from any type `α` to a type `G` that has a subtraction monoid structure, the support of the negated function, that is the set of points `x` in `α` where `-f(x)` is not zero, is the same as the support of the function `f` itself, i.e., the set of points `x` in `α` where `f(x)` is not zero. Essentially, this theorem indicates that negating a function does not change the set of points where the function is non-zero.
More concisely: For a function `f` from type `α` to a subtraction monoid `G`, the sets of points `x` in `α` where `f(x)` and `-f(x)` are non-zero are equal.
|
Function.mulSupport_comp_eq_preimage
theorem Function.mulSupport_comp_eq_preimage :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : One M] (g : β → M) (f : α → β),
Function.mulSupport (g ∘ f) = f ⁻¹' Function.mulSupport g
The theorem `Function.mulSupport_comp_eq_preimage` states that for any types `α`, `β`, and `M` with `M` being a type with a specified identity element, and given any function `g` from `β` to `M` and a function `f` from `α` to `β`, the `mulSupport` of the composition of `g` and `f` (denoted as `g ∘ f`) is equal to the preimage of the `mulSupport` of `g` under the function `f`. In other words, the set of points `x` in `α` such that `(g ∘ f)(x)` is not equal to `1` is exactly the set of points `x` in `α` such that `f(x)` is in the `mulSupport` of `g`.
More concisely: The `Function.mulSupport_comp_eq_preimage` theorem asserts that the sets of points `x` in `α` such that `(g ∘ f)(x) ≠ 1` are equal to the preimage under `f` of the points in the `mulSupport` of `g` in `β`.
|
Function.mulSupport_eq_empty_iff
theorem Function.mulSupport_eq_empty_iff :
∀ {α : Type u_1} {M : Type u_5} [inst : One M] {f : α → M}, Function.mulSupport f = ∅ ↔ f = 1
The theorem `Function.mulSupport_eq_empty_iff` states that for any type `α`, a type `M` with a defined "one" element, and a function `f` from `α` to `M`, the `mulSupport` of `f` is an empty set if and only if `f` is a constant function returning the "one" element of `M`. In other words, the `mulSupport` of `f` contains no elements precisely when `f(x)` equals "one" for all `x` in `α`.
More concisely: For any type α and a function f from α to a type M with a "one" element, the set of multiples of f is empty if and only if f is the constant function mapping all of α to the "one" element of M.
|
Function.support_eq_empty_iff
theorem Function.support_eq_empty_iff :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α → M}, Function.support f = ∅ ↔ f = 0
This theorem states that for any types `α` and `M`, with `M` being a type with a zero element, and for any function `f` from `α` to `M`, the support of `f` is empty if and only if `f` is the zero function. In other words, if all the values of `f` are zero (i.e., `f` is the zero function), then there are no points `x` in `α` for which `f(x) ≠ 0`, and therefore the support of `f` is an empty set. Conversely, if the support of `f` is an empty set, there are no points `x` in `α` for which `f(x) ≠ 0`, which means `f` is the zero function.
More concisely: For any type `α` and type `M` with a zero element, a function `f` from `α` to `M` is the zero function if and only if the support of `f` is empty.
|
Function.mulSupport_const
theorem Function.mulSupport_const :
∀ {α : Type u_1} {M : Type u_5} [inst : One M] {c : M}, c ≠ 1 → (Function.mulSupport fun x => c) = Set.univ := by
sorry
The theorem `Function.mulSupport_const` states that for any types `α` and `M` with `M` having an instance of the `One` typeclass, and any element `c` of `M` that is not equal to `1`, the `mulSupport` of a constant function `f` that always returns `c` is equivalent to the universal set over `α`. In other words, every element `x` of type `α` is such that `f(x)` (which is always `c`) is not equal to `1`.
More concisely: For any type `α` and constant function `f : α → M` with `M` being an instance of `One` and `c ≠ 1` in `M`, the support of `f` (as a function from `α` to `{1, ≠1}`) equals the universal set `α`.
|
Function.support_subset_iff'
theorem Function.support_subset_iff' :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α → M} {s : Set α},
Function.support f ⊆ s ↔ ∀ x ∉ s, f x = 0
The theorem `Function.support_subset_iff'` states that for any types `α` and `M`, given a zero instance for `M`, a function `f` from `α` to `M`, and a set `s` of `α`, the support of the function `f` is a subset of the set `s` if and only if for all elements `x` not in the set `s`, the function `f` evaluated at `x` equals `0`. Here, the support of a function `f` is defined as the set of points `x` such that `f(x)` is not equal to `0`.
More concisely: For functions from type `α` to type `M` with a zero element `0_M`, the support of the function equals the subset of domain `α` where the function does not equal `0_M`. That is, `support(f) ⊆ s` if and only if for all `x ∈ α \ s`, `f(x) = 0_M`.
|
Function.mem_support
theorem Function.mem_support :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α → M} {x : α}, x ∈ Function.support f ↔ f x ≠ 0
This theorem, `Function.mem_support`, states that for all types `α` and `M` with `M` having an instance of the `Zero` class, and for any function `f` from `α` to `M` and any element `x` of `α`, `x` is an element of the support of the function `f` if and only if the function `f` applied to `x` is not equal to zero. In mathematical terms, this can be written as \(x \in \text{supp}(f) \iff f(x) \neq 0\), where \(\text{supp}(f)\) represents the support of the function `f`.
More concisely: The support of a function from type `α` to a type `M` with `M` having an instance of the `Zero` class, contains an element `x` of `α` if and only if the function applied to `x` is non-zero.
|
Mathlib.Algebra.Function.Support._auxLemma.4
theorem Mathlib.Algebra.Function.Support._auxLemma.4 :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α → M} {s : Set α},
(Function.support f ⊆ s) = ∀ (x : α), f x ≠ 0 → x ∈ s
This theorem states that for any given types `α` and `M`, where `M` is a type with a zero element, and for any function `f` from `α` to `M` and any set `s` of elements of type `α`, the support of the function `f` (i.e., the set of points `x` in `α` where `f(x)` is not zero) is a subset of `s` if and only if for every element `x` in `α`, if `f(x)` is not zero, then `x` is an element of `s`. The support of a function is used in this theorem to denote the set of points where the function does not equal zero.
More concisely: For any function from type `α` to a type `M` with a zero element, the support of the function is subset of a given set `s` if and only if every non-zero value of the function belongs to `s`.
|
Function.mulSupport_one
theorem Function.mulSupport_one :
∀ {α : Type u_1} {M : Type u_5} [inst : One M], (Function.mulSupport fun x => 1) = ∅
The theorem `Function.mulSupport_one` states that for any type `α` and any type `M` that has an instance of the `One` typeclass (i.e., has a defined "one" or identity element), the multiplicative support of the constant function that maps every element of `α` to `1` in `M` is the empty set. This is because the multiplicative support of a function consists of all values `x` for which the function applied to `x` is not equal to `1`, but in this case, the function is defined to always return `1` for all inputs. Therefore, there are no values in `α` for which the function does not return `1`, and the multiplicative support is empty.
More concisely: The constant function mapping every element of a type `α` to `1` in a commutative monoid `M` with a defined one element has an empty multiplicative support.
|
Function.mulSupport_one_sub
theorem Function.mulSupport_one_sub :
∀ {α : Type u_1} {R : Type u_8} [inst : One R] [inst_1 : AddGroup R] (f : α → R),
(Function.mulSupport fun x => 1 - f x) = Function.support f
The theorem `Function.mulSupport_one_sub` states that for any function `f` whose domain is of type `α` and codomain is of an additive group `R` that also has a unit element, the multiplicative support of the function `g(x) = 1 - f(x)` is equal to the support of `f`. Here, the multiplicative support of a function is the set of all points in the domain where the function does not output the multiplicative identity (which is `1` in this context), and the support of a function is the set of all points in the domain where the function does not output the additive identity (`0` in this context). Thus, this theorem establishes a relationship between these two different "nonzeroness-tracking" measures applied to related functions.
More concisely: For a function from type `α` to an additive group with unit element, the multiplicative support equals the negation of the support of the function mapping `x` to `1 - f(x)`.
|
Function.support_zero
theorem Function.support_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M], (Function.support fun x => 0) = ∅ := by
sorry
The theorem `Function.support_zero` states that for any types `α` and `M` where `M` has a zero element, the function support of a constant zero function (a function mapping any element from `α` to zero) is an empty set. In other words, there are no elements `x` in `α` for which the function value `f x` is not equal to zero, since all elements map to zero.
More concisely: For any type `α` and any constant function `f : α → ℤ` with value 0, the function support of `f` is empty.
|
Mathlib.Algebra.Function.Support._auxLemma.2
theorem Mathlib.Algebra.Function.Support._auxLemma.2 :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α → M} {x : α}, (x ∈ Function.support f) = (f x ≠ 0) := by
sorry
The theorem `Mathlib.Algebra.Function.Support._auxLemma.2` states that for any type `α`, any type `M` with a zero element, any function `f` from `α` to `M`, and any element `x` of type `α`, the element `x` belongs to the support of function `f` if and only if the function `f` at `x` is not equal to zero. In other words, a point `x` is in the support of a function `f` precisely when `f(x)` is nonzero.
More concisely: A function's support equals the set of arguments where the function does not equal the zero element.
|
Function.support_const
theorem Function.support_const :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {c : M}, c ≠ 0 → (Function.support fun x => c) = Set.univ := by
sorry
This theorem, named `Function.support_const`, states that for any types `α` and `M`, given that `M` has a zero element and any constant `c` from `M` that is not equal to zero, the support of the function that maps any element of `α` to the constant `c` is the universal set. In other words, if a function always returns a nonzero constant, then its support (the set of all input values for which the function is nonzero) is the entire set of all possible input values.
More concisely: For any type `α` and constant `c ≠ 0` in a type `M` with zero element, the function `λ x : α, c` has support equal to the universe `α`.
|
Function.nmem_support
theorem Function.nmem_support :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α → M} {x : α}, x ∉ Function.support f ↔ f x = 0
The theorem `Function.nmem_support` states that for any types `α` and `M` with `M` having an instance of `Zero` and for any function `f` from `α` to `M` and any element `x` of `α`, `x` is not in the support of `f` if and only if `f(x)` equals zero. In other words, an element is not in the support of a function (defined as the set of points where the function does not equal zero) if and only if the function evaluated at that element is equal to zero.
More concisely: The theorem `Function.nmem_support` asserts that an element is not in the support of a function if and only if the function evaluates to zero at that element.
|
Function.support_comp_subset
theorem Function.support_comp_subset :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : Zero M] [inst_1 : Zero N] {g : M → N},
g 0 = 0 → ∀ (f : α → M), Function.support (g ∘ f) ⊆ Function.support f
This theorem states that for all types `α`, `M`, and `N`, where `M` and `N` are equipped with a zero element, given a function `g` from `M` to `N` that maps zero to zero, and any function `f` from `α` to `M`, the support of the composition `g ∘ f` is a subset of the support of `f`. In other words, for any element in the domain, if the composed function `g ∘ f` is non-zero at that point, then the function `f` must also be non-zero at that point.
More concisely: Given functions `g: M -> N` with `g 0 = 0` and `f: α -> M`, the support of `g ∘ f` is contained in the support of `f`.
|
Function.mulSupport_subset_iff'
theorem Function.mulSupport_subset_iff' :
∀ {α : Type u_1} {M : Type u_5} [inst : One M] {f : α → M} {s : Set α},
Function.mulSupport f ⊆ s ↔ ∀ x ∉ s, f x = 1
This theorem is stating that for any given types `α` and `M`, where `M` has an instance of `One` (meaning it has a designated "one" element), and any function `f` from `α` to `M`, and any set `s` of elements of type `α`, the `mulSupport` of `f` (which is the set of points `x` where `f(x)` is not equal to `1`) is a subset of `s` if and only if for every `x` that is not in `s`, `f(x)` equals `1`. In other words, if a point `x` is not in set `s`, then the value of the function `f` at `x` must be `1`, and this condition is both necessary and sufficient to ensure that all points where `f` does not equal `1` are contained within `s`.
More concisely: For any function `f` from type `α` to a type `M` with a `One` instance, the set `{x : α | f x ≠ 1}` is a subset of a set `s` if and only if for all `x ∈ α \ s`, we have `f x = 1`.
|
Function.support_zero'
theorem Function.support_zero' : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M], Function.support 0 = ∅
This theorem states that for any types `α` and `M` where `M` is equipped with a zero, the support of the zero function (a function always returning zero) is the empty set. In other words, there are no elements `x` from `α` such that `0(x) ≠ 0`, since the zero function always returns `0` for any `x`, making its support set empty.
More concisely: For any type `α` and zeroed type `M`, the support of the zero function is empty.
|
Function.support_binop_subset
theorem Function.support_binop_subset :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P]
(op : M → N → P),
op 0 0 = 0 →
∀ (f : α → M) (g : α → N),
(Function.support fun x => op (f x) (g x)) ⊆ Function.support f ∪ Function.support g
The theorem `Function.support_binop_subset` states that for any types `α`, `M`, `N`, and `P`, where `M`, `N`, and `P` all have a `Zero` instance, and for any binary operation `op` from `M` and `N` to `P` that satisfies `op 0 0 = 0`, for any functions `f` from `α` to `M` and `g` from `α` to `N`, the support (set of points where the function is not zero) of the function `x => op (f x) (g x)` is a subset of the union of the supports of functions `f` and `g`. This theorem essentially conveys that any point where the composed operation produces a non-zero result must also be a point where either `f` or `g` (or both) produce a non-zero result.
More concisely: For functions `f : α → M` and `g : α → N` with types having `Zero` instances, and a binary operation `op : M × N → P` satisfying `op 0 0 = 0`, the support of `x => op (f x) (g x)` is contained in the union of the supports of `f` and `g`.
|