Module docstring
{"# Piecewise functions
This file contains basic results on piecewise defined functions. "}
Set.piecewise_empty
theorem
[∀ i : α, Decidable (i ∈ (∅ : Set α))] : piecewise ∅ f g = g
Full source
@[simp]
theorem piecewise_empty [∀ i : α, Decidable (i ∈ (∅ : Set α))] : piecewise ∅ f g = g := by
ext i
simp [piecewise]Informal description
For any type $\alpha$ with decidable membership in the empty set, and for any functions $f, g : \alpha \to \beta$, the piecewise function defined on the empty set satisfies $\text{piecewise}\ \emptyset\ f\ g = g$. In other words, the piecewise function defaults to $g$ everywhere when the set is empty.
Set.piecewise_univ
theorem
[∀ i : α, Decidable (i ∈ (Set.univ : Set α))] : piecewise Set.univ f g = f
Full source
@[simp]
theorem piecewise_univ [∀ i : α, Decidable (i ∈ (Set.univ : Set α))] :
piecewise Set.univ f g = f := by
ext i
simp [piecewise]Informal description
For any type $\alpha$ with decidable membership in the universal set, and for any functions $f, g : \alpha \to \beta$, the piecewise function defined on the universal set satisfies $\text{piecewise}\ \text{univ}\ f\ g = f$. In other words, the piecewise function equals $f$ everywhere when the set is the universal set.
Set.piecewise_insert_self
theorem
{j : α} [∀ i, Decidable (i ∈ insert j s)] : (insert j s).piecewise f g j = f j
Full source
theorem piecewise_insert_self {j : α} [∀ i, Decidable (i ∈ insert j s)] :
(insert j s).piecewise f g j = f j := by simp [piecewise]Informal description
For any element $j$ of type $\alpha$ and any set $s \subseteq \alpha$ with decidable membership, the piecewise function defined on the set $\{j\} \cup s$ satisfies $(s \cup \{j\}).\text{piecewise}\ f\ g\ j = f(j)$. In other words, at the point $j$, the piecewise function takes the value of the first function $f$.
Set.piecewise_insert
theorem
[DecidableEq α] (j : α) [∀ i, Decidable (i ∈ insert j s)] :
(insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j)
Full source
theorem piecewise_insert [DecidableEq α] (j : α) [∀ i, Decidable (i ∈ insert j s)] :
(insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j) := by
simp +unfoldPartialApp only [piecewise, mem_insert_iff]
ext i
by_cases h : i = j
· rw [h]
simp
· by_cases h' : i ∈ s <;> simp [h, h']Informal description
For a type $\alpha$ with decidable equality, given a set $s \subseteq \alpha$, a point $j \in \alpha$, and functions $f, g : \alpha \to \beta$, the piecewise function on the set $\text{insert } j \, s$ satisfies:
\[
(\text{insert } j \, s).\text{piecewise}\ f\ g = \text{update } (s.\text{piecewise}\ f\ g) \, j \, (f j)
\]
where the right-hand side updates the piecewise function on $s$ at $j$ with the value $f j$.
Set.piecewise_eq_of_mem
theorem
{i : α} (hi : i ∈ s) : s.piecewise f g i = f i
Full source
@[simp]
theorem piecewise_eq_of_mem {i : α} (hi : i ∈ s) : s.piecewise f g i = f i :=
if_pos hiInformal description
For any element $i$ in the set $s$, the piecewise function defined by $s$, $f$, and $g$ evaluated at $i$ equals $f(i)$, i.e., $(s.\text{piecewise}\ f\ g)(i) = f(i)$.
Set.piecewise_eq_of_not_mem
theorem
{i : α} (hi : i ∉ s) : s.piecewise f g i = g i
Full source
@[simp]
theorem piecewise_eq_of_not_mem {i : α} (hi : i ∉ s) : s.piecewise f g i = g i :=
if_neg hiInformal description
For any element $i$ not in the set $s$, the piecewise function $s.\text{piecewise}\ f\ g$ evaluated at $i$ equals $g(i)$, i.e., $(s.\text{piecewise}\ f\ g)(i) = g(i)$.
Set.piecewise_singleton
theorem
(x : α) [∀ y, Decidable (y ∈ ({ x } : Set α))] [DecidableEq α] (f g : α → β) :
piecewise { x } f g = Function.update g x (f x)
Full source
theorem piecewise_singleton (x : α) [∀ y, Decidable (y ∈ ({x} : Set α))] [DecidableEq α]
(f g : α → β) : piecewise {x} f g = Function.update g x (f x) := by
ext y
by_cases hy : y = x
· subst y
simp
· simp [hy]Informal description
For any element $x$ of type $\alpha$, and any functions $f, g : \alpha \to \beta$, the piecewise function defined on the singleton set $\{x\}$ is equal to the function obtained by updating $g$ at $x$ with the value $f(x)$. That is,
\[
\{x\}.\text{piecewise}\ f\ g = \text{update}\ g\ x\ (f x).
\]
Here, the condition $y \in \{x\}$ is decidable for each $y \in \alpha$, and $\alpha$ has decidable equality.
Set.piecewise_eqOn
theorem
(f g : α → β) : EqOn (s.piecewise f g) f s
Full source
theorem piecewise_eqOn (f g : α → β) : EqOn (s.piecewise f g) f s := fun _ =>
piecewise_eq_of_mem _ _ _Informal description
For any functions $f, g : \alpha \to \beta$ and any set $s \subseteq \alpha$, the piecewise function $s.\text{piecewise}\ f\ g$ is equal to $f$ on the set $s$. That is, for all $x \in s$, we have $(s.\text{piecewise}\ f\ g)(x) = f(x)$.
Set.piecewise_eqOn_compl
theorem
(f g : α → β) : EqOn (s.piecewise f g) g sᶜ
Full source
theorem piecewise_eqOn_compl (f g : α → β) : EqOn (s.piecewise f g) g sᶜ := fun _ =>
piecewise_eq_of_not_mem _ _ _Informal description
For any functions $f, g : \alpha \to \beta$ and any set $s \subseteq \alpha$, the piecewise function $s.\text{piecewise}\ f\ g$ is equal to $g$ on the complement of $s$. That is, for all $x \notin s$, we have $(s.\text{piecewise}\ f\ g)(x) = g(x)$.
Set.piecewise_le
theorem
{δ : α → Type*} [∀ i, Preorder (δ i)] {s : Set α} [∀ j, Decidable (j ∈ s)] {f₁ f₂ g : ∀ i, δ i}
(h₁ : ∀ i ∈ s, f₁ i ≤ g i) (h₂ : ∀ i ∉ s, f₂ i ≤ g i) : s.piecewise f₁ f₂ ≤ g
Full source
theorem piecewise_le {δ : α → Type*} [∀ i, Preorder (δ i)] {s : Set α} [∀ j, Decidable (j ∈ s)]
{f₁ f₂ g : ∀ i, δ i} (h₁ : ∀ i ∈ s, f₁ i ≤ g i) (h₂ : ∀ i ∉ s, f₂ i ≤ g i) :
s.piecewise f₁ f₂ ≤ g := fun i => if h : i ∈ s then by simp [*] else by simp [*]Informal description
Let $\alpha$ be a type, $\delta : \alpha \to \text{Type}^*$ a family of types with a preorder structure on each $\delta(i)$, and $s \subseteq \alpha$ a decidable subset. Given functions $f_1, f_2, g : \forall i, \delta(i)$, if for all $i \in s$ we have $f_1(i) \leq g(i)$, and for all $i \notin s$ we have $f_2(i) \leq g(i)$, then the piecewise function defined by $s$, $f_1$, and $f_2$ is pointwise less than or equal to $g$. That is, for all $i \in \alpha$, we have $(s.\text{piecewise}\ f_1\ f_2)(i) \leq g(i)$.
Set.le_piecewise
theorem
{δ : α → Type*} [∀ i, Preorder (δ i)] {s : Set α} [∀ j, Decidable (j ∈ s)] {f₁ f₂ g : ∀ i, δ i}
(h₁ : ∀ i ∈ s, g i ≤ f₁ i) (h₂ : ∀ i ∉ s, g i ≤ f₂ i) : g ≤ s.piecewise f₁ f₂
Full source
theorem le_piecewise {δ : α → Type*} [∀ i, Preorder (δ i)] {s : Set α} [∀ j, Decidable (j ∈ s)]
{f₁ f₂ g : ∀ i, δ i} (h₁ : ∀ i ∈ s, g i ≤ f₁ i) (h₂ : ∀ i ∉ s, g i ≤ f₂ i) :
g ≤ s.piecewise f₁ f₂ :=
@piecewise_le α (fun i => (δ i)ᵒᵈ) _ s _ _ _ _ h₁ h₂Informal description
Let $\alpha$ be a type, $\delta : \alpha \to \text{Type}^*$ a family of types with a preorder structure on each $\delta(i)$, and $s \subseteq \alpha$ a decidable subset. Given functions $f_1, f_2, g : \forall i, \delta(i)$, if for all $i \in s$ we have $g(i) \leq f_1(i)$, and for all $i \notin s$ we have $g(i) \leq f_2(i)$, then $g$ is pointwise less than or equal to the piecewise function defined by $s$, $f_1$, and $f_2$. That is, for all $i \in \alpha$, we have $g(i) \leq (s.\text{piecewise}\ f_1\ f_2)(i)$.
Set.piecewise_mono
theorem
{δ : α → Type*} [∀ i, Preorder (δ i)] {s : Set α} [∀ j, Decidable (j ∈ s)] {f₁ f₂ g₁ g₂ : ∀ i, δ i}
(h₁ : ∀ i ∈ s, f₁ i ≤ g₁ i) (h₂ : ∀ i ∉ s, f₂ i ≤ g₂ i) : s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂
Full source
@[gcongr]
theorem piecewise_mono {δ : α → Type*} [∀ i, Preorder (δ i)] {s : Set α}
[∀ j, Decidable (j ∈ s)] {f₁ f₂ g₁ g₂ : ∀ i, δ i} (h₁ : ∀ i ∈ s, f₁ i ≤ g₁ i)
(h₂ : ∀ i ∉ s, f₂ i ≤ g₂ i) : s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂ := by
apply piecewise_le <;> intros <;> simp [*]Informal description
Let $\alpha$ be a type, $\delta : \alpha \to \text{Type}^*$ a family of types with a preorder structure on each $\delta(i)$, and $s \subseteq \alpha$ a decidable subset. Given functions $f_1, f_2, g_1, g_2 : \forall i, \delta(i)$, if for all $i \in s$ we have $f_1(i) \leq g_1(i)$, and for all $i \notin s$ we have $f_2(i) \leq g_2(i)$, then the piecewise function defined by $s$, $f_1$, and $f_2$ is pointwise less than or equal to the piecewise function defined by $s$, $g_1$, and $g_2$. That is, for all $i \in \alpha$, we have $(s.\text{piecewise}\ f_1\ f_2)(i) \leq (s.\text{piecewise}\ g_1\ g_2)(i)$.
Set.piecewise_insert_of_ne
theorem
{i j : α} (h : i ≠ j) [∀ i, Decidable (i ∈ insert j s)] : (insert j s).piecewise f g i = s.piecewise f g i
Full source
@[simp]
theorem piecewise_insert_of_ne {i j : α} (h : i ≠ j) [∀ i, Decidable (i ∈ insert j s)] :
(insert j s).piecewise f g i = s.piecewise f g i := by simp [piecewise, h]Informal description
For any distinct elements $i$ and $j$ of type $\alpha$, and for any set $s \subseteq \alpha$ with decidable membership, the piecewise function defined on the set $s \cup \{j\}$ evaluated at $i$ is equal to the piecewise function defined on $s$ evaluated at $i$, i.e.,
\[
(s \cup \{j\}).\text{piecewise}\ f\ g\ (i) = s.\text{piecewise}\ f\ g\ (i).
\]
Set.piecewise_compl
theorem
[∀ i, Decidable (i ∈ sᶜ)] : sᶜ.piecewise f g = s.piecewise g f
Full source
@[simp]
theorem piecewise_compl [∀ i, Decidable (i ∈ sᶜ)] : sᶜ.piecewise f g = s.piecewise g f :=
funext fun x => if hx : x ∈ s then by simp [hx] else by simp [hx]Informal description
For any set $s \subseteq \alpha$ with decidable membership, the piecewise function defined on the complement $s^c$ with components $f$ and $g$ is equal to the piecewise function defined on $s$ with components $g$ and $f$, i.e.,
\[
s^c.\text{piecewise}\ f\ g = s.\text{piecewise}\ g\ f.
\]
Set.piecewise_range_comp
theorem
{ι : Sort*} (f : ι → α) [∀ j, Decidable (j ∈ range f)] (g₁ g₂ : α → β) : (range f).piecewise g₁ g₂ ∘ f = g₁ ∘ f
Full source
@[simp]
theorem piecewise_range_comp {ι : Sort*} (f : ι → α) [∀ j, Decidable (j ∈ range f)]
(g₁ g₂ : α → β) : (range f).piecewise g₁ g₂ ∘ f = g₁ ∘ f :=
(piecewise_eqOn ..).comp_eqInformal description
Let $f : \iota \to \alpha$ be a function with decidable membership in its range, and let $g_1, g_2 : \alpha \to \beta$ be functions. Then the composition of the piecewise function defined on the range of $f$ with $f$ equals the composition of $g_1$ with $f$, i.e.,
\[
(\text{range } f).\text{piecewise}\ g_1\ g_2 \circ f = g_1 \circ f.
\]
Set.piecewise_comp
theorem
(f g : α → γ) (h : β → α) :
letI : DecidablePred (· ∈ h ⁻¹' s) := @instDecidablePredComp _ (· ∈ s) _ h _;
(s.piecewise f g) ∘ h = (h ⁻¹' s).piecewise (f ∘ h) (g ∘ h)
Full source
lemma piecewise_comp (f g : α → γ) (h : β → α) :
letI : DecidablePred (· ∈ h ⁻¹' s) := @instDecidablePredComp _ (· ∈ s) _ h _;
(s.piecewise f g) ∘ h = (h⁻¹' s).piecewise (f ∘ h) (g ∘ h) := by
ext x
by_cases hx : h x ∈ s <;> simp [hx]Informal description
Let $f, g : \alpha \to \gamma$ and $h : \beta \to \alpha$ be functions, and let $s \subseteq \alpha$ be a set with decidable membership. Then the composition of the piecewise function $s.\text{piecewise}\ f\ g$ with $h$ is equal to the piecewise function defined on the preimage $h^{-1}(s) \subseteq \beta$ with components $f \circ h$ and $g \circ h$:
\[
(s.\text{piecewise}\ f\ g) \circ h = (h^{-1}(s)).\text{piecewise}\ (f \circ h)\ (g \circ h).
\]
Set.MapsTo.piecewise_ite
theorem
{s s₁ s₂ : Set α} {t t₁ t₂ : Set β} {f₁ f₂ : α → β} [∀ i, Decidable (i ∈ s)] (h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t))
(h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)) : MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)
Full source
theorem MapsTo.piecewise_ite {s s₁ s₂ : Set α} {t t₁ t₂ : Set β} {f₁ f₂ : α → β}
[∀ i, Decidable (i ∈ s)] (h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t))
(h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)) :
MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂) := by
refine (h₁.congr ?_).union_union (h₂.congr ?_)
exacts [(piecewise_eqOn s f₁ f₂).symm.mono inter_subset_right,
(piecewise_eqOn_compl s f₁ f₂).symm.mono inter_subset_right]Informal description
Let $s, s_1, s_2 \subseteq \alpha$ and $t, t_1, t_2 \subseteq \beta$ be sets, and let $f_1, f_2 : \alpha \to \beta$ be functions. Suppose that:
1. $f_1$ maps $s_1 \cap s$ into $t_1 \cap t$, and
2. $f_2$ maps $s_2 \cap s^c$ into $t_2 \cap t^c$.
Then the piecewise function $s.\text{piecewise}\ f_1\ f_2$ maps the set $\text{ite}(s, s_1, s_2) = (s \cap s_1) \cup (s^c \cap s_2)$ into the set $\text{ite}(t, t_1, t_2) = (t \cap t_1) \cup (t^c \cap t_2)$.
Set.eqOn_piecewise
theorem
{f f' g : α → β} {t} : EqOn (s.piecewise f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ)
Full source
theorem eqOn_piecewise {f f' g : α → β} {t} :
EqOnEqOn (s.piecewise f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ) := by
simp only [EqOn, ← forall_and]
refine forall_congr' fun a => ?_; by_cases a ∈ s <;> simp [*]Informal description
For functions $f, f', g : \alpha \to \beta$ and a set $t \subseteq \alpha$, the piecewise function $s.\text{piecewise}\ f\ f'$ is equal to $g$ on $t$ if and only if $f$ is equal to $g$ on $t \cap s$ and $f'$ is equal to $g$ on $t \cap s^c$. In other words:
\[
(s.\text{piecewise}\ f\ f') = g \text{ on } t \quad \Leftrightarrow \quad f = g \text{ on } t \cap s \text{ and } f' = g \text{ on } t \cap s^c.
\]
Set.EqOn.piecewise_ite'
theorem
{f f' g : α → β} {t t'} (h : EqOn f g (t ∩ s)) (h' : EqOn f' g (t' ∩ sᶜ)) : EqOn (s.piecewise f f') g (s.ite t t')
Full source
theorem EqOn.piecewise_ite' {f f' g : α → β} {t t'} (h : EqOn f g (t ∩ s))
(h' : EqOn f' g (t' ∩ sᶜ)) : EqOn (s.piecewise f f') g (s.ite t t') := by
simp [eqOn_piecewise, *]Informal description
Let $f, f', g : \alpha \to \beta$ be functions and $s, t, t' \subseteq \alpha$ be sets. If $f$ coincides with $g$ on $t \cap s$ and $f'$ coincides with $g$ on $t' \cap s^c$, then the piecewise function $s.\text{piecewise}\, f\, f'$ coincides with $g$ on the set $\text{ite}(s, t, t') = (s \cap t) \cup (s^c \cap t')$.
Set.EqOn.piecewise_ite
theorem
{f f' g : α → β} {t t'} (h : EqOn f g t) (h' : EqOn f' g t') : EqOn (s.piecewise f f') g (s.ite t t')
Full source
theorem EqOn.piecewise_ite {f f' g : α → β} {t t'} (h : EqOn f g t) (h' : EqOn f' g t') :
EqOn (s.piecewise f f') g (s.ite t t') :=
(h.mono inter_subset_left).piecewise_ite' s (h'.mono inter_subset_left)Informal description
Let $f, f', g : \alpha \to \beta$ be functions and $s, t, t' \subseteq \alpha$ be sets. If $f$ coincides with $g$ on $t$ and $f'$ coincides with $g$ on $t'$, then the piecewise function $s.\text{piecewise}\, f\, f'$ coincides with $g$ on the set $\text{ite}(s, t, t') = (s \cap t) \cup (s^c \cap t')$.
Set.piecewise_preimage
theorem
(f g : α → β) (t) : s.piecewise f g ⁻¹' t = s.ite (f ⁻¹' t) (g ⁻¹' t)
Full source
theorem piecewise_preimage (f g : α → β) (t) : s.piecewise f g ⁻¹' t = s.ite (f ⁻¹' t) (g ⁻¹' t) :=
ext fun x => by by_cases x ∈ s <;> simp [*, Set.ite]Informal description
For any set $s \subseteq \alpha$ and functions $f, g : \alpha \to \beta$, the preimage of a set $t \subseteq \beta$ under the piecewise function $s.\text{piecewise}\, f\, g$ is equal to the set operation $s.\text{ite}\, (f^{-1}(t))\, (g^{-1}(t))$, where:
\[
(s.\text{piecewise}\, f\, g)^{-1}(t) = s \cap f^{-1}(t) \cup s^c \cap g^{-1}(t).
\]
Here, $s^c$ denotes the complement of $s$ in $\alpha$.
Set.apply_piecewise
theorem
{δ' : α → Sort*} (h : ∀ i, δ i → δ' i) {x : α} :
h x (s.piecewise f g x) = s.piecewise (fun x => h x (f x)) (fun x => h x (g x)) x
Full source
theorem apply_piecewise {δ' : α → Sort*} (h : ∀ i, δ i → δ' i) {x : α} :
h x (s.piecewise f g x) = s.piecewise (fun x => h x (f x)) (fun x => h x (g x)) x := by
by_cases hx : x ∈ s <;> simp [hx]Informal description
Let $s$ be a set in a type $\alpha$, and let $f, g : \forall i, \delta i$ be functions. For any function $h : \forall i, \delta i \to \delta' i$ and any element $x \in \alpha$, we have:
\[
h_x \big(s.\text{piecewise}\, f\, g\, x\big) = \big(s.\text{piecewise}\, (\lambda x, h_x (f x))\, (\lambda x, h_x (g x))\big)\, x,
\]
where $s.\text{piecewise}\, f\, g$ is the piecewise function equal to $f$ on $s$ and $g$ on its complement.
Set.apply_piecewise₂
theorem
{δ' δ'' : α → Sort*} (f' g' : ∀ i, δ' i) (h : ∀ i, δ i → δ' i → δ'' i) {x : α} :
h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x => h x (f x) (f' x)) (fun x => h x (g x) (g' x)) x
Full source
theorem apply_piecewise₂ {δ' δ'' : α → Sort*} (f' g' : ∀ i, δ' i) (h : ∀ i, δ i → δ' i → δ'' i)
{x : α} :
h x (s.piecewise f g x) (s.piecewise f' g' x) =
s.piecewise (fun x => h x (f x) (f' x)) (fun x => h x (g x) (g' x)) x := by
by_cases hx : x ∈ s <;> simp [hx]Informal description
Let $s$ be a set in a type $\alpha$, and let $f, g : \forall i, \delta i$ and $f', g' : \forall i, \delta' i$ be functions. For any function $h : \forall i, \delta i \to \delta' i \to \delta'' i$ and any element $x \in \alpha$, we have:
\[
h_x \big(s.\text{piecewise}\, f\, g\, x\big) \big(s.\text{piecewise}\, f'\, g'\, x\big) = \big(s.\text{piecewise}\, (\lambda x, h_x (f x) (f' x))\, (\lambda x, h_x (g x) (g' x))\big)\, x,
\]
where $s.\text{piecewise}\, f\, g$ is the piecewise function equal to $f$ on $s$ and $g$ on its complement.
Set.piecewise_op
theorem
{δ' : α → Sort*} (h : ∀ i, δ i → δ' i) :
(s.piecewise (fun x => h x (f x)) fun x => h x (g x)) = fun x => h x (s.piecewise f g x)
Full source
theorem piecewise_op {δ' : α → Sort*} (h : ∀ i, δ i → δ' i) :
(s.piecewise (fun x => h x (f x)) fun x => h x (g x)) = fun x => h x (s.piecewise f g x) :=
funext fun _ => (apply_piecewise _ _ _ _).symmInformal description
Let $s$ be a set in a type $\alpha$, and let $f, g : \forall i, \delta i$ be functions. For any function $h : \forall i, \delta i \to \delta' i$, the piecewise function defined by $s$ and the compositions $h \circ f$ and $h \circ g$ is equal to the composition of $h$ with the piecewise function defined by $s$, $f$, and $g$. That is,
\[
s.\text{piecewise}\, (h \circ f)\, (h \circ g) = h \circ (s.\text{piecewise}\, f\, g).
\]
Set.piecewise_op₂
theorem
{δ' δ'' : α → Sort*} (f' g' : ∀ i, δ' i) (h : ∀ i, δ i → δ' i → δ'' i) :
(s.piecewise (fun x => h x (f x) (f' x)) fun x => h x (g x) (g' x)) = fun x =>
h x (s.piecewise f g x) (s.piecewise f' g' x)
Full source
theorem piecewise_op₂ {δ' δ'' : α → Sort*} (f' g' : ∀ i, δ' i) (h : ∀ i, δ i → δ' i → δ'' i) :
(s.piecewise (fun x => h x (f x) (f' x)) fun x => h x (g x) (g' x)) = fun x =>
h x (s.piecewise f g x) (s.piecewise f' g' x) :=
funext fun _ => (apply_piecewise₂ _ _ _ _ _ _).symmInformal description
Let $s$ be a set in a type $\alpha$, and let $f, g : \alpha \to \delta$ and $f', g' : \alpha \to \delta'$ be functions. For any binary function $h : \alpha \to \delta \to \delta' \to \delta''$, the piecewise function defined by:
\[
x \mapsto
\begin{cases}
h_x (f x) (f' x) & \text{if } x \in s, \\
h_x (g x) (g' x) & \text{otherwise,}
\end{cases}
\]
is equal to the function:
\[
x \mapsto h_x \big(s.\text{piecewise}\, f\, g\, x\big) \big(s.\text{piecewise}\, f'\, g'\, x\big).
\]
Here, $s.\text{piecewise}\, f\, g$ denotes the piecewise function equal to $f$ on $s$ and $g$ on its complement.
Set.piecewise_same
theorem
: s.piecewise f f = f
Full source
@[simp]
theorem piecewise_same : s.piecewise f f = f := by
ext x
by_cases hx : x ∈ s <;> simp [hx]Informal description
For any set $s \subseteq \alpha$ and any function $f : \alpha \to \beta$, the piecewise function defined by $s$ and $f$ on both branches is equal to $f$ itself, i.e.,
\[
s.\text{piecewise}\ f\ f = f.
\]
Set.range_piecewise
theorem
(f g : α → β) : range (s.piecewise f g) = f '' s ∪ g '' sᶜ
Full source
theorem range_piecewise (f g : α → β) : range (s.piecewise f g) = f '' sf '' s ∪ g '' sᶜ := by
ext y; constructor
· rintro ⟨x, rfl⟩
by_cases h : x ∈ s <;> [left; right] <;> use x <;> simp [h]
· rintro (⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩) <;> use x <;> simp_allInformal description
For any set $s \subseteq \alpha$ and functions $f, g : \alpha \to \beta$, the range of the piecewise function $s.\text{piecewise}\ f\ g$ is equal to the union of the image of $f$ restricted to $s$ and the image of $g$ restricted to the complement of $s$. That is,
\[
\text{range}(s.\text{piecewise}\ f\ g) = f(s) \cup g(s^c).
\]
Set.injective_piecewise_iff
theorem
{f g : α → β} : Injective (s.piecewise f g) ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y
Full source
theorem injective_piecewise_iff {f g : α → β} :
InjectiveInjective (s.piecewise f g) ↔
InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y := by
rw [injective_iff_injOn_univ, ← union_compl_self s, injOn_union (@disjoint_compl_right _ _ s),
(piecewise_eqOn s f g).injOn_iff, (piecewise_eqOn_compl s f g).injOn_iff]
refine and_congr Iff.rfl (and_congr Iff.rfl <| forall₄_congr fun x hx y hy => ?_)
rw [piecewise_eq_of_mem s f g hx, piecewise_eq_of_not_mem s f g hy]Informal description
Let $f, g : \alpha \to \beta$ be functions and $s \subseteq \alpha$ a set. The piecewise function defined by $s$, $f$, and $g$ is injective if and only if the following three conditions hold:
1. $f$ is injective on $s$,
2. $g$ is injective on the complement $s^c$, and
3. For all $x \in s$ and $y \notin s$, we have $f(x) \neq g(y)$.
Set.piecewise_mem_pi
theorem
{δ : α → Type*} {t : Set α} {t' : ∀ i, Set (δ i)} {f g} (hf : f ∈ pi t t') (hg : g ∈ pi t t') :
s.piecewise f g ∈ pi t t'
Full source
theorem piecewise_mem_pi {δ : α → Type*} {t : Set α} {t' : ∀ i, Set (δ i)} {f g} (hf : f ∈ pi t t')
(hg : g ∈ pi t t') : s.piecewise f g ∈ pi t t' := by
intro i ht
by_cases hs : i ∈ s <;> simp [hf i ht, hg i ht, hs]Informal description
Let $\delta : \alpha \to \mathrm{Type}$ be a type family, $t \subseteq \alpha$ a subset, and $t'$ a family of sets where $t'(i) \subseteq \delta(i)$ for each $i \in \alpha$. Given two functions $f, g : \prod_{i \in \alpha} \delta(i)$ such that $f \in \prod_{i \in t} t'(i)$ and $g \in \prod_{i \in t} t'(i)$, the piecewise function $s.\text{piecewise}\ f\ g$ belongs to $\prod_{i \in t} t'(i)$.
In other words, if $f$ and $g$ both map every $i \in t$ into $t'(i)$, then their piecewise combination (defined by $s$) also maps every $i \in t$ into $t'(i)$.
Set.pi_piecewise
theorem
{ι : Type*} {α : ι → Type*} (s s' : Set ι) (t t' : ∀ i, Set (α i)) [∀ x, Decidable (x ∈ s')] :
pi s (s'.piecewise t t') = pi (s ∩ s') t ∩ pi (s \ s') t'
Full source
@[simp]
theorem pi_piecewise {ι : Type*} {α : ι → Type*} (s s' : Set ι) (t t' : ∀ i, Set (α i))
[∀ x, Decidable (x ∈ s')] : pi s (s'.piecewise t t') = pipi (s ∩ s') t ∩ pi (s \ s') t' :=
pi_if _ _ _Informal description
Let $\iota$ be a type, $\alpha : \iota \to \mathrm{Type}$ a type family, and $s, s' \subseteq \iota$ subsets with membership in $s'$ decidable. For two families of sets $t, t' : \forall i, \mathrm{Set}\, (\alpha i)$, the product set $\prod_{i \in s} (s'.\mathrm{piecewise}\, t\, t')(i)$ is equal to the intersection of the product sets $\prod_{i \in s \cap s'} t(i)$ and $\prod_{i \in s \setminus s'} t'(i)$.
In other words, the product of piecewise-defined sets over $s$ (where each component is $t(i)$ if $i \in s'$ and $t'(i)$ otherwise) decomposes into the intersection of the product over $s \cap s'$ using $t$ and the product over $s \setminus s'$ using $t'$.
Set.univ_pi_piecewise
theorem
{ι : Type*} {α : ι → Type*} (s : Set ι) (t t' : ∀ i, Set (α i)) [∀ x, Decidable (x ∈ s)] :
pi univ (s.piecewise t t') = pi s t ∩ pi sᶜ t'
Full source
theorem univ_pi_piecewise {ι : Type*} {α : ι → Type*} (s : Set ι) (t t' : ∀ i, Set (α i))
[∀ x, Decidable (x ∈ s)] : pi univ (s.piecewise t t') = pipi s t ∩ pi sᶜ t' := by
simp [compl_eq_univ_diff]Informal description
Let $\iota$ be a type, $\alpha : \iota \to \mathrm{Type}$ a type family, and $s \subseteq \iota$ a subset with decidable membership. For any two families of sets $t, t' : \forall i, \mathrm{Set}\, (\alpha i)$, the product set $\prod_{i \in \mathrm{univ}} (s.\mathrm{piecewise}\, t\, t')(i)$ over the universal set equals the intersection of the product sets $\prod_{i \in s} t(i)$ and $\prod_{i \in s^c} t'(i)$.
In other words:
\[
\prod_{i \in \iota} \begin{cases}
t(i) & \text{if } i \in s, \\
t'(i) & \text{otherwise}
\end{cases} = \left(\prod_{i \in s} t(i)\right) \cap \left(\prod_{i \in \iota \setminus s} t'(i)\right)
\]
Set.univ_pi_piecewise_univ
theorem
{ι : Type*} {α : ι → Type*} (s : Set ι) (t : ∀ i, Set (α i)) [∀ x, Decidable (x ∈ s)] :
pi univ (s.piecewise t fun _ => univ) = pi s t
Informal description
Let $\iota$ be a type and $\alpha : \iota \to \mathrm{Type}$ a type family. For any subset $s \subseteq \iota$ with decidable membership and any family of sets $t : \forall i, \mathrm{Set}\, (\alpha i)$, the product set $\prod_{i \in \iota} (s.\mathrm{piecewise}\, t\, \mathrm{univ})(i)$ equals the product set $\prod_{i \in s} t(i)$.
In other words, the product over the universal index set $\iota$ of the piecewise function (which equals $t(i)$ when $i \in s$ and the universal set $\alpha_i$ otherwise) reduces to the product of $t(i)$ over $s$.