Piecewise functions

This file contains basic results on piecewise defined functions.

@[simp]

theorem Set.piecewise_empty {α : Type u_1} {δ : α → Sort u_6} (f g : (i : α) → δ i) [(i : α) → Decidable (i ∈ ∅)] : ∅.piecewise f g = g

@[simp]

theorem Set.piecewise_univ {α : Type u_1} {δ : α → Sort u_6} (f g : (i : α) → δ i) [(i : α) → Decidable (i ∈ univ)] : univ.piecewise f g = f

theorem Set.piecewise_insert_self {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) {j : α} [(i : α) → Decidable (i ∈ insert j s)] : (insert j s).piecewise f g j = f j

theorem Set.piecewise_insert {α : Type u_1} {δ : α → Sort u_6} (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)

@[simp]

theorem Set.piecewise_eq_of_mem {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {i : α} (hi : i ∈ s) : s.piecewise f g i = f i

@[simp]

theorem Set.piecewise_eq_of_notMem {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {i : α} (hi : ¬i ∈ s) : s.piecewise f g i = g i

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)

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

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ᶜ

theorem Set.piecewise_le {α : Type u_1} {δ : α → Type u_7} [(i : α) → Preorder (δ i)] {s : Set α} [(j : α) → Decidable (j ∈ s)] {f₁ f₂ g : (i : α) → δ i} (h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g i) (h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g i) : s.piecewise f₁ f₂ ≤ g

theorem Set.le_piecewise {α : Type u_1} {δ : α → Type u_7} [(i : α) → Preorder (δ i)] {s : Set α} [(j : α) → Decidable (j ∈ s)] {f₁ f₂ g : (i : α) → δ i} (h₁ : ∀ (i : α), i ∈ s → g i ≤ f₁ i) (h₂ : ∀ (i : α), ¬i ∈ s → g i ≤ f₂ i) : g ≤ s.piecewise f₁ f₂

theorem Set.piecewise_mono {α : Type u_1} {δ : α → Type u_7} [(i : α) → Preorder (δ i)] {s : Set α} [(j : α) → Decidable (j ∈ s)] {f₁ f₂ g₁ g₂ : (i : α) → δ i} (h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i) (h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i) : s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂

@[simp]

theorem Set.piecewise_insert_of_ne {α : Type u_1} {δ : α → Sort u_6} (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

@[simp]

theorem Set.piecewise_compl {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] [(i : α) → Decidable (i ∈ sᶜ)] : sᶜ.piecewise f g = s.piecewise g f

@[simp]

theorem Set.piecewise_range_comp {α : Type u_1} {β : Type u_2} {ι : Sort u_7} (f : ι → α) [(j : α) → Decidable (j ∈ range f)] (g₁ g₂ : α → β) : (range f).piecewise g₁ g₂ ∘ f = g₁ ∘ f

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)

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₂)

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ᶜ)

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')

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')

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)

theorem Set.apply_piecewise {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {δ' : α → Sort u_7} (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

theorem Set.apply_piecewise₂ {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {δ' : α → Sort u_7} {δ'' : α → Sort u_8} (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

theorem Set.piecewise_op {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {δ' : α → Sort u_7} (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)

theorem Set.piecewise_op₂ {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] {δ' : α → Sort u_7} {δ'' : α → Sort u_8} (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)

@[simp]

theorem Set.piecewise_same {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] : s.piecewise f f = f

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ᶜ

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 : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y

theorem Set.piecewise_mem_pi {α : Type u_1} (s : Set α) [(j : α) → Decidable (j ∈ s)] {δ : α → Type u_7} {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'

@[simp]

theorem Set.pi_piecewise {ι : Type u_7} {α : ι → Type u_8} (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'

theorem Set.univ_pi_piecewise {ι : Type u_7} {α : ι → Type u_8} (s : Set ι) (t t' : (i : ι) → Set (α i)) [(x : ι) → Decidable (x ∈ s)] : univ.pi (s.piecewise t t') = s.pi t ∩ sᶜ.pi t'

theorem Set.univ_pi_piecewise_univ {ι : Type u_7} {α : ι → Type u_8} (s : Set ι) (t : (i : ι) → Set (α i)) [(x : ι) → Decidable (x ∈ s)] : univ.pi (s.piecewise t fun (x : ι) => univ) = s.pi t