DFinsupp.mem_neLocus
theorem DFinsupp.mem_neLocus :
∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
[inst_2 : (a : α) → Zero (N a)] {f g : Π₀ (a : α), N a} {a : α}, a ∈ f.neLocus g ↔ f a ≠ g a
The theorem `DFinsupp.mem_neLocus` states that for any types `α` and `N`, where `N` is a type dependent on `α`, and given `f` and `g` as two finitely supported functions mapping from `α` to `N`, along with an element `a` of type `α`, `a` belongs to the set where `f` and `g` differ (i.e., `DFinsupp.neLocus f g`) if and only if `f(a)` is not equal to `g(a)`. This theorem holds under the conditions that equality is decidable for `α` and for every `N a`, and zero is defined for every `N a`.
More concisely: For functions `f` and `g` mapping from type `α` to type-dependent `N` with decidable equality and defined zero, `a` is in the set of differences if and only if `f(a) ≠ g(a)`.
|
DFinsupp.neLocus_comm
theorem DFinsupp.neLocus_comm :
∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
[inst_2 : (a : α) → Zero (N a)] (f g : Π₀ (a : α), N a), f.neLocus g = g.neLocus f
This theorem states that for any type `α`, and any type `N` that depends on `α`, with both `α` and `N a` having decidable equality and `N a` having a zero element, the function `DFinsupp.neLocus` is commutative. This means that for any two finitely supported functions `f` and `g` (each mapping elements of type `α` to elements of type `N a`), the set of elements of `α` where `f` and `g` differ (given by `DFinsupp.neLocus f g`) is the same as the set of elements where `g` and `f` differ (given by `DFinsupp.neLocus g f`). In other words, the order in which the functions `f` and `g` are presented to `DFinsupp.neLocus` does not affect the outcome.
More concisely: For any type `α` and type `N` depending on `α` with decidable equality and a zero element, the sets `DFinsupp.neLocus` of two finitely supported functions `f` and `g` mapping elements of type `α` to `N a` are equal: `DFinsupp.neLocus f g = DFinsupp.neLocus g f`.
|
Mathlib.Data.DFinsupp.NeLocus._auxLemma.5
theorem Mathlib.Data.DFinsupp.NeLocus._auxLemma.5 :
∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
[inst_2 : (a : α) → Zero (N a)] {f g : Π₀ (a : α), N a} {a : α}, (a ∈ f.neLocus g) = (f a ≠ g a)
This theorem states that for any types `α` and `N` (where `N` is a function on `α`), given the instances of decidable equality for `α` and `N a` for any `a` in `α`, and given the instance of the `Zero` type class for `N a`, if `f` and `g` are two functions of type `(Π₀ (a : α), N a)`, and `a` is of type `α`, then `a` is in the set where `f` and `g` differ (`DFinsupp.neLocus f g`) if and only if `f a` is not equal to `g a`. In other words, `DFinsupp.neLocus f g` consists exactly of those elements of `α` where `f` and `g` do not have the same value.
More concisely: For functions `f` and `g` over a type `α` with decidable equality and where `N` is a function on `α`, the sets `{a : α | f a ≠ g a}` and `DFinsupp.neLocus f g` are equal.
|