Mathlib.Data.Finset.Piecewise

Finset.piecewise definition

[∀ j, Decidable (j ∈ s)] : ∀ i, π i

Full source

/-- `s.piecewise f g` is the function equal to `f` on the finset `s`, and to `g` on its
complement. -/
def piecewise [∀ j, Decidable (j ∈ s)] : ∀ i, π i := fun i ↦ if i ∈ s then f i else g i

Piecewise function on a finite set

Informal description

Given a finite set $s$ of type $\alpha$, and two functions $f, g : \alpha \to \pi$, the function $s.\text{piecewise}\ f\ g$ is defined as: \[ (s.\text{piecewise}\ f\ g)(i) = \begin{cases} f(i) & \text{if } i \in s, \\ g(i) & \text{otherwise.} \end{cases} \]

Finset.piecewise_insert_self theorem

[DecidableEq ι] {j : ι} [∀ i, Decidable (i ∈ insert j s)] : (insert j s).piecewise f g j = f j

Full source

lemma piecewise_insert_self [DecidableEq ι] {j : ι} [∀ i, Decidable (i ∈ insert j s)] :
    (insert j s).piecewise f g j = f j := by simp [piecewise]

Value of Piecewise Function at Inserted Point

Informal description

For any finite set $s$ of type $\iota$, any element $j \in \iota$, and any functions $f, g : \iota \to \pi$, the piecewise function defined on the finite set $\{j\} \cup s$ satisfies \[ (\{j\} \cup s).\text{piecewise}\ f\ g\ (j) = f(j). \]

Finset.piecewise_empty theorem

[∀ i : ι, Decidable (i ∈ (∅ : Finset ι))] : piecewise ∅ f g = g

Full source

@[simp]
lemma piecewise_empty [∀ i : ι, Decidable (i ∈ (∅ : Finset ι))] : piecewise ∅ f g = g := by
  ext i
  simp [piecewise]

Empty Finite Set Piecewise Function Equals $g$

Informal description

For any type $\iota$ and functions $f, g : \iota \to \pi$, the piecewise function defined on the empty finite set $\emptyset \subseteq \iota$ equals $g$, i.e., \[ \emptyset.\text{piecewise}\ f\ g = g. \]

Finset.piecewise_coe theorem

[∀ j, Decidable (j ∈ (s : Set ι))] : (s : Set ι).piecewise f g = s.piecewise f g

Full source

@[norm_cast move]
lemma piecewise_coe [∀ j, Decidable (j ∈ (s : Set ι))] :
    (s : Set ι).piecewise f g = s.piecewise f g := by
  ext
  congr

Equality of Piecewise Functions on Finite Sets and Their Set Counterparts

Informal description

Given a finite set $s$ of type $\iota$, and two functions $f, g : \iota \to \pi$, the piecewise function defined on the set $s$ (viewed as a subset of $\iota$) coincides with the piecewise function defined on the finite set $s$. That is, for all $i \in \iota$, \[ (s : \text{Set } \iota).\text{piecewise}\ f\ g\ i = s.\text{piecewise}\ f\ g\ i. \] Here, the condition $i \in s$ is decidable for each $i \in \iota$.

Finset.piecewise_eq_of_mem theorem

{i : ι} (hi : i ∈ s) : s.piecewise f g i = f i

Full source

@[simp]
lemma piecewise_eq_of_mem {i : ι} (hi : i ∈ s) : s.piecewise f g i = f i := by
  simp [piecewise, hi]

Piecewise Function Equals $f$ on Finite Set Membership

Informal description

For any element $i$ in a finite set $s \subseteq \iota$, the piecewise function $s.\text{piecewise}\ f\ g$ evaluated at $i$ equals $f(i)$, i.e., \[ s.\text{piecewise}\ f\ g\ i = f(i). \]

Finset.piecewise_eq_of_not_mem theorem

{i : ι} (hi : i ∉ s) : s.piecewise f g i = g i

Full source

@[simp]
lemma piecewise_eq_of_not_mem {i : ι} (hi : i ∉ s) : s.piecewise f g i = g i := by
  simp [piecewise, hi]

Piecewise Function Equals $g$ Outside Finite Set

Informal description

For any element $i$ not in a finite set $s \subseteq \iota$, the piecewise function $s.\text{piecewise}\ f\ g$ evaluated at $i$ equals $g(i)$, i.e., \[ s.\text{piecewise}\ f\ g\ i = g(i). \]

Finset.piecewise_congr theorem

 {f f' g g' : ∀ i, π i} (hf : ∀ i ∈ s, f i = f' i) (hg : ∀ i ∉ s, g i = g' i) : s.piecewise f g = s.piecewise f' g'

Full source

lemma piecewise_congr {f f' g g' : ∀ i, π i} (hf : ∀ i ∈ s, f i = f' i)
    (hg : ∀ i ∉ s, g i = g' i) : s.piecewise f g = s.piecewise f' g' :=
  funext fun i => if_ctx_congr Iff.rfl (hf i) (hg i)

Congruence for Piecewise Functions on Finite Sets

Informal description

Let $s$ be a finite subset of a type $\alpha$, and let $f, f', g, g'$ be functions from $\alpha$ to some type $\pi$. If $f(i) = f'(i)$ for all $i \in s$ and $g(i) = g'(i)$ for all $i \notin s$, then the piecewise functions defined by $s$ using $(f, g)$ and $(f', g')$ are equal, i.e., \[ s.\text{piecewise}\ f\ g = s.\text{piecewise}\ f'\ g'. \]

Finset.piecewise_insert_of_ne theorem

 [DecidableEq ι] {i j : ι} [∀ i, Decidable (i ∈ insert j s)] (h : i ≠ j) :
  (insert j s).piecewise f g i = s.piecewise f g i

Full source

@[simp]
lemma piecewise_insert_of_ne [DecidableEq ι] {i j : ι} [∀ i, Decidable (i ∈ insert j s)]
    (h : i ≠ j) : (insert j s).piecewise f g i = s.piecewise f g i := by simp [piecewise, h]

Piecewise Function on Inserted Set for Distinct Points

Informal description

Let $s$ be a finite subset of a type $\iota$ with decidable equality, and let $f, g$ be functions from $\iota$ to some type $\pi$. For any distinct elements $i, j \in \iota$, the piecewise function defined on the set $\{j\} \cup s$ evaluated at $i$ is equal to the piecewise function defined on $s$ evaluated at $i$, i.e., \[ (\{j\} \cup s).\text{piecewise}\ f\ g\ i = s.\text{piecewise}\ f\ g\ i. \]

Finset.piecewise_insert theorem

 [DecidableEq ι] (j : ι) [∀ i, Decidable (i ∈ insert j s)] :
  (insert j s).piecewise f g = update (s.piecewise f g) j (f j)

Full source

lemma piecewise_insert [DecidableEq ι] (j : ι) [∀ i, Decidable (i ∈ insert j s)] :
    (insert j s).piecewise f g = update (s.piecewise f g) j (f j) := by
  classical simp only [← piecewise_coe, coe_insert, ← Set.piecewise_insert]
  ext
  congr
  simp

Piecewise Function on Inserted Set as Update

Informal description

Let $\iota$ be a type with decidable equality, $s$ a finite subset of $\iota$, and $f, g : \iota \to \pi$ functions. For any $j \in \iota$, the piecewise function defined on $\{j\} \cup s$ is equal to updating the piecewise function defined on $s$ at the point $j$ with the value $f(j)$. That is, \[ (\{j\} \cup s).\text{piecewise}\ f\ g = \text{update}\ (s.\text{piecewise}\ f\ g)\ j\ (f\ j). \]

Finset.piecewise_cases theorem

{i} (p : π i → Prop) (hf : p (f i)) (hg : p (g i)) : p (s.piecewise f g i)

Full source

lemma piecewise_cases {i} (p : π i → Prop) (hf : p (f i)) (hg : p (g i)) :
    p (s.piecewise f g i) := by
  by_cases hi : i ∈ s <;> simpa [hi]

Predicate Preservation Under Piecewise Construction

Informal description

For any element $i$ of type $\iota$ and any predicate $p$ on $\pi\ i$, if $p(f\ i)$ and $p(g\ i)$ both hold, then $p$ also holds for the piecewise function $s.\text{piecewise}\ f\ g$ evaluated at $i$, i.e., $p(s.\text{piecewise}\ f\ g\ i)$.

Finset.piecewise_singleton theorem

[DecidableEq ι] (i : ι) : piecewise { i } f g = update g i (f i)

Full source

lemma piecewise_singleton [DecidableEq ι] (i : ι) : piecewise {i} f g = update g i (f i) := by
  rw [← insert_empty_eq, piecewise_insert, piecewise_empty]

Singleton Piecewise Function as Update: $\{i\}.\text{piecewise}\ f\ g = \text{update}\ g\ i\ (f\ i)$

Informal description

For any type $\iota$ with decidable equality and any element $i \in \iota$, the piecewise function defined on the singleton set $\{i\}$ with functions $f, g : \iota \to \pi$ is equal to updating the function $g$ at the point $i$ with the value $f(i)$. That is, \[ \{i\}.\text{piecewise}\ f\ g = \text{update}\ g\ i\ (f\ i). \]

Finset.piecewise_piecewise_of_subset_left theorem

 {s t : Finset ι} [∀ i, Decidable (i ∈ s)] [∀ i, Decidable (i ∈ t)] (h : s ⊆ t) (f₁ f₂ g : ∀ a, π a) :
  s.piecewise (t.piecewise f₁ f₂) g = s.piecewise f₁ g

Full source

lemma piecewise_piecewise_of_subset_left {s t : Finset ι} [∀ i, Decidable (i ∈ s)]
    [∀ i, Decidable (i ∈ t)] (h : s ⊆ t) (f₁ f₂ g : ∀ a, π a) :
    s.piecewise (t.piecewise f₁ f₂) g = s.piecewise f₁ g :=
  s.piecewise_congr (fun _i hi => piecewise_eq_of_mem _ _ _ (h hi)) fun _ _ => rfl

Nested Piecewise Function Simplification for Subset Condition

Informal description

Let $s$ and $t$ be finite subsets of a type $\iota$ with $s \subseteq t$, and let $f_1, f_2, g : \iota \to \pi$ be functions. Then the piecewise function defined by $s$ using $(t.\text{piecewise}\ f_1\ f_2, g)$ is equal to the piecewise function defined by $s$ using $(f_1, g)$, i.e., \[ s.\text{piecewise}\ (t.\text{piecewise}\ f_1\ f_2)\ g = s.\text{piecewise}\ f_1\ g. \]

Finset.piecewise_idem_left theorem

(f₁ f₂ g : ∀ a, π a) : s.piecewise (s.piecewise f₁ f₂) g = s.piecewise f₁ g

Full source

@[simp]
lemma piecewise_idem_left (f₁ f₂ g : ∀ a, π a) :
    s.piecewise (s.piecewise f₁ f₂) g = s.piecewise f₁ g :=
  piecewise_piecewise_of_subset_left (Subset.refl _) _ _ _

Idempotence of Left Piecewise Function on Finite Sets

Informal description

For any finite set $s$ of type $\iota$ and functions $f_1, f_2, g : \iota \to \pi$, the piecewise function defined by $s$ using $(s.\text{piecewise}\ f_1\ f_2, g)$ is equal to the piecewise function defined by $s$ using $(f_1, g)$, i.e., \[ s.\text{piecewise}\ (s.\text{piecewise}\ f_1\ f_2)\ g = s.\text{piecewise}\ f_1\ g. \]

Finset.piecewise_piecewise_of_subset_right theorem

 {s t : Finset ι} [∀ i, Decidable (i ∈ s)] [∀ i, Decidable (i ∈ t)] (h : t ⊆ s) (f g₁ g₂ : ∀ a, π a) :
  s.piecewise f (t.piecewise g₁ g₂) = s.piecewise f g₂

Full source

lemma piecewise_piecewise_of_subset_right {s t : Finset ι} [∀ i, Decidable (i ∈ s)]
    [∀ i, Decidable (i ∈ t)] (h : t ⊆ s) (f g₁ g₂ : ∀ a, π a) :
    s.piecewise f (t.piecewise g₁ g₂) = s.piecewise f g₂ :=
  s.piecewise_congr (fun _ _ => rfl) fun _i hi => t.piecewise_eq_of_not_mem _ _ (mt (@h _) hi)

Nested Piecewise Function Simplification for Subset Relation

Informal description

Let $s$ and $t$ be finite subsets of a type $\iota$ with $t \subseteq s$, and let $f, g_1, g_2$ be functions from $\iota$ to some type $\pi$. Then the piecewise function defined by $s$ using $f$ and the piecewise function defined by $t$ using $g_1$ and $g_2$ is equal to the piecewise function defined by $s$ using $f$ and $g_2$, i.e., \[ s.\text{piecewise}\ f\ (t.\text{piecewise}\ g_1\ g_2) = s.\text{piecewise}\ f\ g_2. \]

Finset.piecewise_idem_right theorem

(f g₁ g₂ : ∀ a, π a) : s.piecewise f (s.piecewise g₁ g₂) = s.piecewise f g₂

Full source

@[simp]
lemma piecewise_idem_right (f g₁ g₂ : ∀ a, π a) :
    s.piecewise f (s.piecewise g₁ g₂) = s.piecewise f g₂ :=
  piecewise_piecewise_of_subset_right (Subset.refl _) f g₁ g₂

Idempotence of Piecewise Function on the Right

Informal description

For any finite set $s$ of type $\iota$ and functions $f, g_1, g_2 : \iota \to \pi$, the piecewise function defined by $s$ using $f$ and the piecewise function defined by $s$ using $g_1$ and $g_2$ is equal to the piecewise function defined by $s$ using $f$ and $g_2$, i.e., \[ s.\text{piecewise}\ f\ (s.\text{piecewise}\ g_1\ g_2) = s.\text{piecewise}\ f\ g_2. \]

Finset.update_eq_piecewise theorem

{β : Type*} [DecidableEq ι] (f : ι → β) (i : ι) (v : β) : update f i v = piecewise (singleton i) (fun _ => v) f

Full source

lemma update_eq_piecewise {β : Type*} [DecidableEq ι] (f : ι → β) (i : ι) (v : β) :
    update f i v = piecewise (singleton i) (fun _ => v) f :=
  (piecewise_singleton (fun _ => v) _ _).symm

Function Update as Piecewise Function on Singleton Set

Informal description

For any type $\iota$ with decidable equality, function $f : \iota \to \beta$, element $i \in \iota$, and value $v \in \beta$, the update of $f$ at $i$ with value $v$ is equal to the piecewise function defined on the singleton set $\{i\}$ using the constant function $\lambda \_, v$ and $f$. That is, \[ \text{update } f \, i \, v = \{i\}.\text{piecewise}\ (\lambda \_, v)\ f. \]

Finset.update_piecewise theorem

[DecidableEq ι] (i : ι) (v : π i) : update (s.piecewise f g) i v = s.piecewise (update f i v) (update g i v)

Full source

lemma update_piecewise [DecidableEq ι] (i : ι) (v : π i) :
    update (s.piecewise f g) i v = s.piecewise (update f i v) (update g i v) := by
  ext j
  rcases em (j = i) with (rfl | hj) <;> by_cases hs : j ∈ s <;> simp [*]

Update of Piecewise Function Equals Piecewise of Updates

Informal description

For any finite set $s$ of type $\iota$, functions $f, g : \iota \to \pi$, element $i \in \iota$, and value $v \in \pi i$, updating the piecewise function $s.\text{piecewise}\ f\ g$ at $i$ with $v$ is equal to the piecewise combination of the updated functions: \[ \text{update } (s.\text{piecewise}\ f\ g) \, i \, v = s.\text{piecewise}\ (\text{update } f \, i \, v)\ (\text{update } g \, i \, v). \]

Finset.update_piecewise_of_mem theorem

[DecidableEq ι] {i : ι} (hi : i ∈ s) (v : π i) : update (s.piecewise f g) i v = s.piecewise (update f i v) g

Full source

lemma update_piecewise_of_mem [DecidableEq ι] {i : ι} (hi : i ∈ s) (v : π i) :
    update (s.piecewise f g) i v = s.piecewise (update f i v) g := by
  rw [update_piecewise]
  refine s.piecewise_congr (fun _ _ => rfl) fun j hj => update_of_ne ?_ ..
  exact fun h => hj (h.symm ▸ hi)

Update of Piecewise Function at Member Point Equals Piecewise of Updated Function

Informal description

Let $s$ be a finite subset of a type $\iota$, and let $f, g : \iota \to \pi$ be functions. For any element $i \in s$ and any value $v \in \pi i$, updating the piecewise function $s.\text{piecewise}\ f\ g$ at $i$ with $v$ is equal to the piecewise combination of the updated function $\text{update } f \, i \, v$ and the original function $g$: \[ \text{update } (s.\text{piecewise}\ f\ g) \, i \, v = s.\text{piecewise}\ (\text{update } f \, i \, v)\ g. \]

Finset.update_piecewise_of_not_mem theorem

[DecidableEq ι] {i : ι} (hi : i ∉ s) (v : π i) : update (s.piecewise f g) i v = s.piecewise f (update g i v)

Full source

lemma update_piecewise_of_not_mem [DecidableEq ι] {i : ι} (hi : i ∉ s) (v : π i) :
    update (s.piecewise f g) i v = s.piecewise f (update g i v) := by
  rw [update_piecewise]
  refine s.piecewise_congr (fun j hj => update_of_ne ?_ ..) fun _ _ => rfl
  exact fun h => hi (h ▸ hj)

Update of Piecewise Function Outside the Set Equals Piecewise with Updated Second Function

Informal description

For any finite set $s$ of type $\iota$, functions $f, g : \iota \to \pi$, element $i \in \iota$ such that $i \notin s$, and value $v \in \pi i$, updating the piecewise function $s.\text{piecewise}\ f\ g$ at $i$ with $v$ is equal to the piecewise combination of $f$ and the updated function $\text{update } g \, i \, v$: \[ \text{update } (s.\text{piecewise}\ f\ g) \, i \, v = s.\text{piecewise}\ f\ (\text{update } g \, i \, v). \]

Finset.piecewise_same theorem

: s.piecewise f f = f

Full source

lemma piecewise_same : s.piecewise f f = f := by
  ext i
  by_cases h : i ∈ s <;> simp [h]

Piecewise Function with Identical Components Equals Original Function

Informal description

For any finite set $s \subseteq \iota$ and function $f : \iota \to \pi$, the piecewise function $s.\text{piecewise}\ f\ f$ is equal to $f$ itself, i.e., \[ s.\text{piecewise}\ f\ f = f. \]

Finset.piecewise_univ theorem

[∀ i, Decidable (i ∈ (univ : Finset ι))] (f g : ∀ i, π i) : univ.piecewise f g = f

Full source

@[simp]
lemma piecewise_univ [∀ i, Decidable (i ∈ (univ : Finset ι))] (f g : ∀ i, π i) :
    univ.piecewise f g = f := by
  ext i
  simp [piecewise]

Piecewise Function on Universal Finite Set Coincides with First Function

Informal description

For any finite type $\iota$ and functions $f, g : \iota \to \pi$, the piecewise function defined on the universal finite set $\text{univ} : \text{Finset}\ \iota$ (which contains all elements of $\iota$) satisfies: \[ \text{univ.piecewise}\ f\ g = f. \] In other words, when the piecewise function is defined over the entire finite type, it coincides with the first function $f$.

Finset.piecewise_compl theorem

 [DecidableEq ι] (s : Finset ι) [∀ i, Decidable (i ∈ s)] [∀ i, Decidable (i ∈ sᶜ)] (f g : ∀ i, π i) :
  sᶜ.piecewise f g = s.piecewise g f

Full source

lemma piecewise_compl [DecidableEq ι] (s : Finset ι) [∀ i, Decidable (i ∈ s)]
    [∀ i, Decidable (i ∈ sᶜ)] (f g : ∀ i, π i) :
    sᶜ.piecewise f g = s.piecewise g f := by
  ext i
  simp [piecewise]

Complementary Piecewise Function Equals Swapped Piecewise Function

Informal description

For a finite type $\iota$ with decidable equality, given a finite subset $s \subseteq \iota$ and two functions $f, g : \iota \to \pi$, the piecewise function defined on the complement $s^\complement$ satisfies: \[ s^\complement.\text{piecewise}\ f\ g = s.\text{piecewise}\ g\ f. \] In other words, the piecewise function that uses $f$ on the complement of $s$ and $g$ elsewhere is equal to the piecewise function that uses $g$ on $s$ and $f$ elsewhere.

Finset.piecewise_erase_univ theorem

[DecidableEq ι] (i : ι) (f g : ∀ i, π i) : (Finset.univ.erase i).piecewise f g = Function.update f i (g i)

Full source

@[simp]
lemma piecewise_erase_univ [DecidableEq ι] (i : ι) (f g : ∀ i, π i) :
    (Finset.univ.erase i).piecewise f g = Function.update f i (g i) := by
  rw [← compl_singleton, piecewise_compl, piecewise_singleton]

Piecewise Function on Universal Set Minus Singleton as Function Update

Informal description

For a finite type $\iota$ with decidable equality and any element $i \in \iota$, the piecewise function defined on the universal finite set with $i$ removed satisfies: \[ (\text{univ} \setminus \{i\}).\text{piecewise}\ f\ g = \text{update}\ f\ i\ (g\ i). \] In other words, the piecewise function that uses $f$ everywhere except at $i$ (where it uses $g(i)$) is equal to updating $f$ at $i$ with the value $g(i)$.

Finset.piecewise_mem_set_pi theorem

(hf : f ∈ Set.pi t t') (hg : g ∈ Set.pi t t') : s.piecewise f g ∈ Set.pi t t'

Full source

lemma piecewise_mem_set_pi (hf : f ∈ Set.pi t t') (hg : g ∈ Set.pi t t') :
    s.piecewise f g ∈ Set.pi t t' := by
  classical rw [← piecewise_coe]; exact Set.piecewise_mem_pi (↑s) hf hg

Piecewise Function Preserves Membership in Indexed Product Set

Informal description

Let $s$ be a finite subset of a type $\alpha$, and let $t \subseteq \alpha$ be a subset with an associated family of sets $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 defined by \[ (s.\text{piecewise}\ f\ g)(i) = \begin{cases} f(i) & \text{if } i \in s, \\ g(i) & \text{otherwise}, \end{cases} \] also satisfies $s.\text{piecewise}\ f\ g \in \prod_{i \in t} t'(i)$.

Finset.piecewise_le_of_le_of_le theorem

(hf : f ≤ h) (hg : g ≤ h) : s.piecewise f g ≤ h

Full source

lemma piecewise_le_of_le_of_le (hf : f ≤ h) (hg : g ≤ h) : s.piecewise f g ≤ h := fun x =>
  piecewise_cases s f g (· ≤ h x) (hf x) (hg x)

Piecewise Function is Bounded Above by Common Upper Bound

Informal description

Let $s$ be a finite subset of a type $\iota$, and let $f, g, h$ be functions from $\iota$ to a type $\pi$ equipped with a preorder $\leq$. If $f \leq h$ and $g \leq h$ pointwise, then the piecewise function defined by \[ (s.\text{piecewise}\ f\ g)(i) = \begin{cases} f(i) & \text{if } i \in s, \\ g(i) & \text{otherwise}, \end{cases} \] also satisfies $s.\text{piecewise}\ f\ g \leq h$ pointwise.

Finset.le_piecewise_of_le_of_le theorem

(hf : h ≤ f) (hg : h ≤ g) : h ≤ s.piecewise f g

Full source

lemma le_piecewise_of_le_of_le (hf : h ≤ f) (hg : h ≤ g) : h ≤ s.piecewise f g := fun x =>
  piecewise_cases s f g (fun y => h x ≤ y) (hf x) (hg x)

Lower Bound Preservation Under Piecewise Construction

Informal description

Let $s$ be a finite subset of a type $\iota$, and let $f, g, h$ be functions from $\iota$ to a type $\pi$ equipped with a preorder $\leq$. If $h \leq f$ and $h \leq g$ pointwise, then $h \leq s.\text{piecewise}\ f\ g$ pointwise, i.e., for all $x \in \iota$, we have $h(x) \leq (s.\text{piecewise}\ f\ g)(x)$.

Finset.piecewise_le_piecewise' theorem

(hf : ∀ x ∈ s, f x ≤ f' x) (hg : ∀ x ∉ s, g x ≤ g' x) : s.piecewise f g ≤ s.piecewise f' g'

Full source

lemma piecewise_le_piecewise' (hf : ∀ x ∈ s, f x ≤ f' x) (hg : ∀ x ∉ s, g x ≤ g' x) :
    s.piecewise f g ≤ s.piecewise f' g' := fun x => by by_cases hx : x ∈ s <;> simp [hx, *]

Monotonicity of Piecewise Functions with Respect to Pointwise Order

Informal description

Let $s$ be a finite subset of a type $\iota$, and let $f, g, f', g'$ be functions from $\iota$ to a type $\pi$ equipped with a preorder $\leq$. If $f(x) \leq f'(x)$ for all $x \in s$ and $g(x) \leq g'(x)$ for all $x \notin s$, then the piecewise function $s.\text{piecewise}\ f\ g$ is pointwise less than or equal to $s.\text{piecewise}\ f'\ g'$, i.e., \[ (s.\text{piecewise}\ f\ g)(x) \leq (s.\text{piecewise}\ f'\ g')(x) \quad \text{for all } x \in \iota. \]

Finset.piecewise_le_piecewise theorem

(hf : f ≤ f') (hg : g ≤ g') : s.piecewise f g ≤ s.piecewise f' g'

Full source

lemma piecewise_le_piecewise (hf : f ≤ f') (hg : g ≤ g') : s.piecewise f g ≤ s.piecewise f' g' :=
  s.piecewise_le_piecewise' (fun x _ => hf x) fun x _ => hg x

Monotonicity of Piecewise Functions under Pointwise Order

Informal description

Let $s$ be a finite subset of a type $\iota$, and let $f, g, f', g'$ be functions from $\iota$ to a type $\pi$ equipped with a preorder $\leq$. If $f \leq f'$ and $g \leq g'$ pointwise (i.e., $f(x) \leq f'(x)$ and $g(x) \leq g'(x)$ for all $x \in \iota$), then the piecewise function $s.\text{piecewise}\ f\ g$ is pointwise less than or equal to $s.\text{piecewise}\ f'\ g'$, i.e., \[ (s.\text{piecewise}\ f\ g)(x) \leq (s.\text{piecewise}\ f'\ g')(x) \quad \text{for all } x \in \iota. \]

Finset.piecewise_mem_Icc_of_mem_of_mem theorem

(hf : f ∈ Set.Icc f' g') (hg : g ∈ Set.Icc f' g') : s.piecewise f g ∈ Set.Icc f' g'

Full source

lemma piecewise_mem_Icc_of_mem_of_mem (hf : f ∈ Set.Icc f' g') (hg : g ∈ Set.Icc f' g') :
    s.piecewise f g ∈ Set.Icc f' g' :=
  ⟨le_piecewise_of_le_of_le _ hf.1 hg.1, piecewise_le_of_le_of_le _ hf.2 hg.2⟩

Piecewise Function Preserves Interval Bounds

Informal description

Let $s$ be a finite subset of a type $\iota$, and let $f, g, f', g'$ be functions from $\iota$ to a type $\pi$ equipped with a preorder $\leq$. If $f$ and $g$ are both pointwise bounded below by $f'$ and above by $g'$ (i.e., $f \in [f', g']$ and $g \in [f', g']$), then the piecewise function $s.\text{piecewise}\ f\ g$ is also pointwise bounded below by $f'$ and above by $g'$, i.e., \[ s.\text{piecewise}\ f\ g \in [f', g']. \]

Finset.piecewise_mem_Icc theorem

(h : f ≤ g) : s.piecewise f g ∈ Set.Icc f g

Full source

lemma piecewise_mem_Icc (h : f ≤ g) : s.piecewise f g ∈ Set.Icc f g :=
  piecewise_mem_Icc_of_mem_of_mem _ (Set.left_mem_Icc.2 h) (Set.right_mem_Icc.2 h)

Piecewise Function Lies in Interval $[f, g]$ When $f \leq g$

Informal description

Let $s$ be a finite subset of a type $\iota$, and let $f, g : \iota \to \pi$ be functions where $\pi$ is equipped with a preorder $\leq$. If $f \leq g$ pointwise (i.e., $f(i) \leq g(i)$ for all $i \in \iota$), then the piecewise function $s.\text{piecewise}\ f\ g$ lies within the closed interval $[f, g]$, meaning that for all $i \in \iota$, we have $f(i) \leq (s.\text{piecewise}\ f\ g)(i) \leq g(i)$.

Finset.piecewise_mem_Icc' theorem

(h : g ≤ f) : s.piecewise f g ∈ Set.Icc g f

Full source

lemma piecewise_mem_Icc' (h : g ≤ f) : s.piecewise f g ∈ Set.Icc g f :=
  piecewise_mem_Icc_of_mem_of_mem _ (Set.right_mem_Icc.2 h) (Set.left_mem_Icc.2 h)

Piecewise Function Bounds When $g \leq f$

Informal description

Let $s$ be a finite subset of a type $\iota$, and let $f, g : \iota \to \pi$ be functions where $\pi$ is equipped with a preorder $\leq$. If $g \leq f$ pointwise (i.e., $g(i) \leq f(i)$ for all $i \in \iota$), then the piecewise function $s.\text{piecewise}\ f\ g$ lies within the closed interval $[g, f]$, i.e., for all $i \in \iota$, \[ g(i) \leq (s.\text{piecewise}\ f\ g)(i) \leq f(i). \]

TODO