# Piecewise functions #

This file contains basic results on piecewise defined functions.

source
@[simp]
theorem Set.piecewise_empty {α : Type u_1} {δ : α → Sort u_7} (f g : (i : α) → δ i) [(i : α) → Decidable (i ∈ ∅)] :
∅.piecewise f g = g
source
@[simp]
theorem Set.piecewise_univ {α : Type u_1} {δ : α → Sort u_7} (f g : (i : α) → δ i) [(i : α) → Decidable (i ∈ univ)] :
univ.piecewise f g = f
source
theorem Set.piecewise_insert_self {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) {j : α} [(i : α) → Decidable (i ∈ insert j s)] :
(insert j s).piecewise f g j = f j
source
theorem Set.piecewise_insert {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] [DecidableEq α] (j : α) [(i : α) → Decidable (i ∈ insert j s)] :
(insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j)
source
@[simp]
theorem Set.piecewise_eq_of_mem {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {i : α} (hi : i ∈ s) :
s.piecewise f g i = f i
source
@[simp]
theorem Set.piecewise_eq_of_notMem {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {i : α} (hi : i ∉ s) :
s.piecewise f g i = g i
source
@[deprecated Set.piecewise_eq_of_notMem (since := "2025-05-23")]
theorem Set.piecewise_eq_of_not_mem {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {i : α} (hi : i ∉ s) :
s.piecewise f g i = g i

Alias of `Set.piecewise_eq_of_notMem`.

source
theorem Set.piecewise_singleton {α : Type u_1} {β : Type u_2} (x : α) [(y : α) → Decidable (y ∈ {x})] [DecidableEq α] (f g : α → β) :
{x}.piecewise f g = Function.update g x (f x)
source
theorem Set.piecewise_eqOn {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j ∈ s)] (f g : α → β) :
EqOn (s.piecewise f g) f s
source
theorem Set.piecewise_eqOn_compl {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j ∈ s)] (f g : α → β) :
EqOn (s.piecewise f g) g s ᶜ
source
theorem Set.piecewise_le {α : Type u_1} {δ : α → Type u_8} [(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
source
theorem Set.le_piecewise {α : Type u_1} {δ : α → Type u_8} [(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₂
source
theorem Set.piecewise_mono {α : Type u_1} {δ : α → Type u_8} [(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₂
source
@[simp]
theorem Set.piecewise_insert_of_ne {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {i j : α} (h : i ≠ j) [(i : α) → Decidable (i ∈ insert j s)] :
(insert j s).piecewise f g i = s.piecewise f g i
source
@[simp]
theorem Set.piecewise_compl {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] [(i : α) → Decidable (i ∈ s ᶜ)] :
s ᶜ.piecewise f g = s.piecewise g f
source
@[simp]
theorem Set.piecewise_range_comp {α : Type u_1} {β : Type u_2} {ι : Sort u_8} (f : ι → α) [(j : α) → Decidable (j ∈ range f)] (g₁ g₂ : α → β) :
(range f).piecewise g₁ g₂ ∘ f = g₁ ∘ f
source
theorem Set.piecewise_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set α) [(j : α) → Decidable (j ∈ s)] (f g : α → γ) (h : β → α) :
s.piecewise f g ∘ h = (h ⁻¹' s).piecewise (f ∘ h) (g ∘ h)
source
theorem Set.MapsTo.piecewise_ite {α : Type u_1} {β : Type u_2} {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₂)
source
theorem Set.eqOn_piecewise {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j ∈ s)] {f f' g : α → β} {t : Set α} :
EqOn (s.piecewise f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ s ᶜ)
source
theorem Set.EqOn.piecewise_ite' {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j ∈ s)] {f f' g : α → β} {t t' : Set α} (h : EqOn f g (t ∩ s)) (h' : EqOn f' g (t' ∩ s ᶜ)) :
EqOn (s.piecewise f f') g (s.ite t t')
source
theorem Set.EqOn.piecewise_ite {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j ∈ s)] {f f' g : α → β} {t t' : Set α} (h : EqOn f g t) (h' : EqOn f' g t') :
EqOn (s.piecewise f f') g (s.ite t t')
source
theorem Set.piecewise_preimage {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j ∈ s)] (f g : α → β) (t : Set β) :
s.piecewise f g ⁻¹' t = s.ite (f ⁻¹' t) (g ⁻¹' t)
source
theorem Set.apply_piecewise {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {δ' : α → Sort u_8} (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
source
theorem Set.apply_piecewise₂ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {δ' : α → Sort u_8} {δ'' : α → Sort u_9} (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
source
theorem Set.piecewise_op {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {δ' : α → Sort u_8} (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)
source
theorem Set.piecewise_op₂ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {δ' : α → Sort u_8} {δ'' : α → Sort u_9} (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)
source
@[simp]
theorem Set.piecewise_same {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] :
s.piecewise f f = f
source
theorem Set.range_piecewise {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j ∈ s)] (f g : α → β) :
range (s.piecewise f g) = f '' s ∪ g '' s ᶜ
source
theorem Set.injective_piecewise_iff {α : Type u_1} {β : Type u_2} (s : Set α) [(j : α) → Decidable (j ∈ s)] {f g : α → β} :
Function.Injective (s.piecewise f g) ↔ InjOn f s ∧ InjOn g s ᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y
source
theorem Set.piecewise_mem_pi {α : Type u_1} (s : Set α) [(j : α) → Decidable (j ∈ s)] {δ : α → Type u_8} {t : Set α} {t' : (i : α) → Set (δ i)} {f g : (i : α) → δ i} (hf : f ∈ t.pi t') (hg : g ∈ t.pi t') :
s.piecewise f g ∈ t.pi t'
source
@[simp]
theorem Set.pi_piecewise {ι : Type u_8} {α : ι → Type u_9} (s s' : Set ι) (t t' : (i : ι) → Set (α i)) [(x : ι) → Decidable (x ∈ s')] :
s.pi (s'.piecewise t t') = (s ∩ s').pi t ∩ (s \ s').pi t'
source
theorem Set.univ_pi_piecewise {ι : Type u_8} {α : ι → Type u_9} (s : Set ι) (t t' : (i : ι) → Set (α i)) [(x : ι) → Decidable (x ∈ s)] :
univ.pi (s.piecewise t t') = s.pi t ∩ s ᶜ.pi t'
source
theorem Set.univ_pi_piecewise_univ {ι : Type u_8} {α : ι → Type u_9} (s : Set ι) (t : (i : ι) → Set (α i)) [(x : ι) → Decidable (x ∈ s)] :
univ.pi (s.piecewise t fun (x : ι) => univ) = s.pi t