Functions defined piecewise on a finset

This file defines Finset.piecewise: Given two functions f, g, s.piecewise f g is a function which is equal to f on s and g on the complement.

TODO

Should we deduplicate this from Set.piecewise?

def Finset.piecewise {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j ∈ s)] (i : ι) : π i

s.piecewise f g is the function equal to f on the finset s, and to g on its complement.

Equations

• Finset.piecewise s f g i = if i ∈ s then f i else g i

theorem Finset.piecewise_insert_self {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) (g : (i : ι) → π i) [DecidableEq ι] {j : ι} [(i : ι) → Decidable (i ∈ insert j s)] : Finset.piecewise (insert j s) f g j = f j

@[simp]

theorem Finset.piecewise_empty {ι : Type u_1} {π : ι → Sort u_2} (f : (i : ι) → π i) (g : (i : ι) → π i) [(i : ι) → Decidable (i ∈ ∅)] : Finset.piecewise ∅ f g = g

theorem Finset.piecewise_coe {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j ∈ s)] [(j : ι) → Decidable (j ∈ ↑s)] : Set.piecewise (↑s) f g = Finset.piecewise s f g

@[simp]

theorem Finset.piecewise_eq_of_mem {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j ∈ s)] {i : ι} (hi : i ∈ s) : Finset.piecewise s f g i = f i

@[simp]

theorem Finset.piecewise_eq_of_not_mem {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j ∈ s)] {i : ι} (hi : i ∉ s) : Finset.piecewise s f g i = g i

theorem Finset.piecewise_congr {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) [(j : ι) → Decidable (j ∈ s)] {f : (i : ι) → π i} {f' : (i : ι) → π i} {g : (i : ι) → π i} {g' : (i : ι) → π i} (hf : ∀ i ∈ s, f i = f' i) (hg : ∀ i ∉ s, g i = g' i) : Finset.piecewise s f g = Finset.piecewise s f' g'

@[simp]

theorem Finset.piecewise_insert_of_ne {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j ∈ s)] [DecidableEq ι] {i : ι} {j : ι} [(i : ι) → Decidable (i ∈ insert j s)] (h : i ≠ j) : Finset.piecewise (insert j s) f g i = Finset.piecewise s f g i

theorem Finset.piecewise_insert {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j ∈ s)] [DecidableEq ι] (j : ι) [(i : ι) → Decidable (i ∈ insert j s)] : Finset.piecewise (insert j s) f g = Function.update (Finset.piecewise s f g) j (f j)

theorem Finset.piecewise_cases {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j ∈ s)] {i : ι} (p : π i → Prop) (hf : p (f i)) (hg : p (g i)) : p (Finset.piecewise s f g i)

theorem Finset.piecewise_singleton {ι : Type u_1} {π : ι → Sort u_2} (f : (i : ι) → π i) (g : (i : ι) → π i) [DecidableEq ι] (i : ι) : Finset.piecewise {i} f g = Function.update g i (f i)

theorem Finset.piecewise_piecewise_of_subset_left {ι : Type u_1} {π : ι → Sort u_2} {s : Finset ι} {t : Finset ι} [(i : ι) → Decidable (i ∈ s)] [(i : ι) → Decidable (i ∈ t)] (h : s ⊆ t) (f₁ : (a : ι) → π a) (f₂ : (a : ι) → π a) (g : (a : ι) → π a) : Finset.piecewise s (Finset.piecewise t f₁ f₂) g = Finset.piecewise s f₁ g

@[simp]

theorem Finset.piecewise_idem_left {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) [(j : ι) → Decidable (j ∈ s)] (f₁ : (a : ι) → π a) (f₂ : (a : ι) → π a) (g : (a : ι) → π a) : Finset.piecewise s (Finset.piecewise s f₁ f₂) g = Finset.piecewise s f₁ g

theorem Finset.piecewise_piecewise_of_subset_right {ι : Type u_1} {π : ι → Sort u_2} {s : Finset ι} {t : Finset ι} [(i : ι) → Decidable (i ∈ s)] [(i : ι) → Decidable (i ∈ t)] (h : t ⊆ s) (f : (a : ι) → π a) (g₁ : (a : ι) → π a) (g₂ : (a : ι) → π a) : Finset.piecewise s f (Finset.piecewise t g₁ g₂) = Finset.piecewise s f g₂

@[simp]

theorem Finset.piecewise_idem_right {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) [(j : ι) → Decidable (j ∈ s)] (f : (a : ι) → π a) (g₁ : (a : ι) → π a) (g₂ : (a : ι) → π a) : Finset.piecewise s f (Finset.piecewise s g₁ g₂) = Finset.piecewise s f g₂

theorem Finset.update_eq_piecewise {ι : Type u_1} {β : Type u_3} [DecidableEq ι] (f : ι → β) (i : ι) (v : β) : Function.update f i v = Finset.piecewise {i} (fun (x : ι) => v) f

theorem Finset.update_piecewise {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j ∈ s)] [DecidableEq ι] (i : ι) (v : π i) : Function.update (Finset.piecewise s f g) i v = Finset.piecewise s (Function.update f i v) (Function.update g i v)

theorem Finset.update_piecewise_of_mem {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j ∈ s)] [DecidableEq ι] {i : ι} (hi : i ∈ s) (v : π i) : Function.update (Finset.piecewise s f g) i v = Finset.piecewise s (Function.update f i v) g

theorem Finset.update_piecewise_of_not_mem {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j ∈ s)] [DecidableEq ι] {i : ι} (hi : i ∉ s) (v : π i) : Function.update (Finset.piecewise s f g) i v = Finset.piecewise s f (Function.update g i v)

theorem Finset.piecewise_same {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) [(j : ι) → Decidable (j ∈ s)] : Finset.piecewise s f f = f

@[simp]

theorem Finset.piecewise_univ {ι : Type u_1} {π : ι → Sort u_2} [Fintype ι] [(i : ι) → Decidable (i ∈ Finset.univ)] (f : (i : ι) → π i) (g : (i : ι) → π i) : Finset.piecewise Finset.univ f g = f

theorem Finset.piecewise_compl {ι : Type u_1} {π : ι → Sort u_2} [Fintype ι] [DecidableEq ι] (s : Finset ι) [(i : ι) → Decidable (i ∈ s)] [(i : ι) → Decidable (i ∈ sᶜ)] (f : (i : ι) → π i) (g : (i : ι) → π i) : Finset.piecewise sᶜ f g = Finset.piecewise s g f

@[simp]

theorem Finset.piecewise_erase_univ {ι : Type u_1} {π : ι → Sort u_2} [Fintype ι] [DecidableEq ι] (i : ι) (f : (i : ι) → π i) (g : (i : ι) → π i) : Finset.piecewise (Finset.erase Finset.univ i) f g = Function.update f i (g i)

theorem Finset.piecewise_mem_set_pi {ι : Type u_1} (s : Finset ι) [(j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {t : Set ι} {t' : (i : ι) → Set (π i)} {f : (i : ι) → π i} {g : (i : ι) → π i} (hf : f ∈ Set.pi t t') (hg : g ∈ Set.pi t t') : Finset.piecewise s f g ∈ Set.pi t t'

theorem Finset.piecewise_le_of_le_of_le {ι : Type u_1} (s : Finset ι) [(j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} {h : (i : ι) → π i} [(i : ι) → Preorder (π i)] (hf : f ≤ h) (hg : g ≤ h) : Finset.piecewise s f g ≤ h

theorem Finset.le_piecewise_of_le_of_le {ι : Type u_1} (s : Finset ι) [(j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} {h : (i : ι) → π i} [(i : ι) → Preorder (π i)] (hf : h ≤ f) (hg : h ≤ g) : h ≤ Finset.piecewise s f g

theorem Finset.piecewise_le_piecewise' {ι : Type u_1} (s : Finset ι) [(j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} {f' : (i : ι) → π i} {g' : (i : ι) → π i} [(i : ι) → Preorder (π i)] (hf : ∀ x ∈ s, f x ≤ f' x) (hg : ∀ x ∉ s, g x ≤ g' x) : Finset.piecewise s f g ≤ Finset.piecewise s f' g'

theorem Finset.piecewise_le_piecewise {ι : Type u_1} (s : Finset ι) [(j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} {f' : (i : ι) → π i} {g' : (i : ι) → π i} [(i : ι) → Preorder (π i)] (hf : f ≤ f') (hg : g ≤ g') : Finset.piecewise s f g ≤ Finset.piecewise s f' g'

theorem Finset.piecewise_mem_Icc_of_mem_of_mem {ι : Type u_1} (s : Finset ι) [(j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} {f' : (i : ι) → π i} {g' : (i : ι) → π i} [(i : ι) → Preorder (π i)] (hf : f ∈ Set.Icc f' g') (hg : g ∈ Set.Icc f' g') : Finset.piecewise s f g ∈ Set.Icc f' g'

theorem Finset.piecewise_mem_Icc {ι : Type u_1} (s : Finset ι) [(j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} [(i : ι) → Preorder (π i)] (h : f ≤ g) : Finset.piecewise s f g ∈ Set.Icc f g

theorem Finset.piecewise_mem_Icc' {ι : Type u_1} (s : Finset ι) [(j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} [(i : ι) → Preorder (π i)] (h : g ≤ f) : Finset.piecewise s f g ∈ Set.Icc g f