Finset.piecewise_eq_of_mem
theorem Finset.piecewise_eq_of_mem :
∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)]
{i : ι}, i ∈ s → s.piecewise f g i = f i
The theorem `Finset.piecewise_eq_of_mem` states that for any given type `ι`, any function `π` mapping `ι` to a sort `u_2`, any finset `s` of `ι`, and any two functions `f` and `g` from `ι` to `π i`, if `i` is an element of the finset `s`, then the `piecewise` function of `s`, `f`, and `g` evaluated at `i` is equal to `f` evaluated at `i`. In other words, the `piecewise` function will select the function `f` for any input which is in the given finset `s`.
More concisely: For any type `ι`, function `π` from `ι` to a sort `u_2`, finset `s` of `ι`, and functions `f` and `g` from `ι` to `π`, if `i ∈ s`, then `(Finset.piecewise s f g) i = f i`.
|
Finset.piecewise_congr
theorem Finset.piecewise_congr :
∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] {f f' g g' : (i : ι) → π i},
(∀ i ∈ s, f i = f' i) → (∀ i ∉ s, g i = g' i) → s.piecewise f g = s.piecewise f' g'
This theorem, `Finset.piecewise_congr`, states that for any type `ι`, a function type `π : ι → Sort u_2`, a finite set `s` of type `ι`, and four functions `f`, `f'`, `g`, `g'` of type `ι → π i`, if `f` and `f'` are equal on the set `s` and `g` and `g'` are equal on the complement of `s`, then the piecewise function defined by `f` and `g` on `s` is equal to the piecewise function defined by `f'` and `g'` on `s`.
In other words, if two pairs of functions agree on a finite set and its complement respectively, the piecewise functions constructed from each pair (where each function is used on the set where it agrees with its counterpart) are the same.
More concisely: If functions $f$, $f'$, $g$, and $g'$ agree with each other on a finite set $s$ and complementarily on their domains, then the piecewise functions $x \mapsto \begin{cases} f(x) & x \in s \\ g(x) & x \notin s \end{cases}$ and $x \mapsto \beginextit{piecewise}~ x \mapsto \begin{cases} f'(x) & x \in s \\ g'(x) & x \notin s \end{cases}$ are equal.
|
Finset.piecewise_eq_of_not_mem
theorem Finset.piecewise_eq_of_not_mem :
∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)]
{i : ι}, i ∉ s → s.piecewise f g i = g i
The theorem `Finset.piecewise_eq_of_not_mem` states that for any type `ι`, any sort `π` indexed by `ι`, any finite set `s` of type `ι`, and any two functions `f` and `g` from `ι` to `π`, if a given element `i` of type `ι` does not belong to the finite set `s`, then the piecewise function defined by `s`, `f`, and `g` at `i` is equal to the value of function `g` at `i`. Here, a piecewise function refers to a function that behaves like `f` for elements in `s`, and behaves like `g` for elements not in `s`. The membership of an element in `s` is determined using a decidable predicate.
More concisely: If `i` is not an element of finite set `s` and `f` is the piecewise function defined by `s`, `f`, and `g`, then `f i = g i`.
|