Finsupp.mem_neLocus
theorem Finsupp.mem_neLocus :
∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] {f g : α →₀ N}
{a : α}, a ∈ f.neLocus g ↔ f a ≠ g a
The theorem `Finsupp.mem_neLocus` states that for any types `α` and `N`, given `DecidableEq` instances for α and N, a `Zero` instance for N, and two finitely supported functions `f` and `g` from `α` to `N`, a member `a` of type `α` is in the finset `Finsupp.neLocus f g` if and only if `f a` is not equal to `g a`. In other words, `Finsupp.neLocus f g` contains exactly those elements of `α` for which `f` and `g` yield different values.
More concisely: Forany types `α` and `N` with Decidable Equation instances, and given zero instances for `N` and finitely supported functions `f` and `g` from `α` to `N`, `Finsupp.neLocus f g` contains exactly the elements `a` in `α` for which `f a ≠ g a`.
|
Finsupp.neLocus_comm
theorem Finsupp.neLocus_comm :
∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] (f g : α →₀ N),
f.neLocus g = g.neLocus f
The theorem `Finsupp.neLocus_comm` states that for any two finitely supported functions `f` and `g` from a type `α` to a type `N` where `N` has a zero and `α` and `N` have decidable equality, the set of elements where `f` and `g` differ (denoted by `Finsupp.neLocus f g`) is the same as the set of elements where `g` and `f` differ (denoted by `Finsupp.neLocus g f`). In other words, the `Finsupp.neLocus` operation is commutative.
More concisely: For any two finitely supported functions `f` and `g` from type `α` to type `N` with `N` having a zero and `α` and `N` having decidable equality, `Finsupp.neLocus f g` equals `Finsupp.neLocus g f`.
|
Mathlib.Data.Finsupp.NeLocus._auxLemma.5
theorem Mathlib.Data.Finsupp.NeLocus._auxLemma.5 :
∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] {f g : α →₀ N}
{a : α}, (a ∈ f.neLocus g) = (f a ≠ g a)
The theorem `Mathlib.Data.Finsupp.NeLocus._auxLemma.5` asserts that for any types `α` and `N`, given that `α` and `N` have decidable equality and `N` has a zero element, for any two finitely supported functions `f` and `g` from `α` to `N`, and for any element `a` from `α`, `a` is in the set where `f` and `g` differ (`Finsupp.neLocus f g`) if and only if `f(a)` is not equal to `g(a)`. In other words, the `neLocus` function correctly identifies the set of elements in `α` where the two functions `f` and `g` differ.
More concisely: For any types `α` with decidable equality and `N` having a zero element, two finitely supported functions `f` and `g` from `α` to `N` have different values at `α` element `a` if and only if `a` belongs to the set of elements where `f` and `g` differ (`Finsupp.neLocus f g`).
|