Documentation

Mathlib.Topology.Piecewise

Continuity of piecewise defined functions #

@[simp]
theorem continuousWithinAt_update_same {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} [DecidableEq α] {y : β} :
@[simp]
theorem continuousAt_update_same {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {x : α} [DecidableEq α] {y : β} :
theorem ContinuousOn.if' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {p : αProp} {f g : αβ} [(a : α) → Decidable (p a)] (hpf : as frontier {a : α | p a}, Filter.Tendsto f (nhdsWithin a (s {a : α | p a})) (nhds (if p a then f a else g a))) (hpg : as frontier {a : α | p a}, Filter.Tendsto g (nhdsWithin a (s {a : α | ¬p a})) (nhds (if p a then f a else g a))) (hf : ContinuousOn f (s {a : α | p a})) (hg : ContinuousOn g (s {a : α | ¬p a})) :
ContinuousOn (fun (a : α) => if p a then f a else g a) s
theorem ContinuousOn.piecewise' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} {s t : Set α} [(a : α) → Decidable (a t)] (hpf : as frontier t, Filter.Tendsto f (nhdsWithin a (s t)) (nhds (t.piecewise f g a))) (hpg : as frontier t, Filter.Tendsto g (nhdsWithin a (s t)) (nhds (t.piecewise f g a))) (hf : ContinuousOn f (s t)) (hg : ContinuousOn g (s t)) :
theorem ContinuousOn.if {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} {s : Set α} {p : αProp} [(a : α) → Decidable (p a)] (hp : as frontier {a : α | p a}, f a = g a) (hf : ContinuousOn f (s closure {a : α | p a})) (hg : ContinuousOn g (s closure {a : α | ¬p a})) :
ContinuousOn (fun (a : α) => if p a then f a else g a) s
theorem ContinuousOn.piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} {s t : Set α} [(a : α) → Decidable (a t)] (ht : as frontier t, f a = g a) (hf : ContinuousOn f (s closure t)) (hg : ContinuousOn g (s closure t)) :
theorem continuous_if' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} {p : αProp} [(a : α) → Decidable (p a)] (hpf : afrontier {x : α | p x}, Filter.Tendsto f (nhdsWithin a {x : α | p x}) (nhds (if p a then f a else g a))) (hpg : afrontier {x : α | p x}, Filter.Tendsto g (nhdsWithin a {x : α | ¬p x}) (nhds (if p a then f a else g a))) (hf : ContinuousOn f {x : α | p x}) (hg : ContinuousOn g {x : α | ¬p x}) :
Continuous fun (a : α) => if p a then f a else g a
theorem continuous_if {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} {p : αProp} [(a : α) → Decidable (p a)] (hp : afrontier {x : α | p x}, f a = g a) (hf : ContinuousOn f (closure {x : α | p x})) (hg : ContinuousOn g (closure {x : α | ¬p x})) :
Continuous fun (a : α) => if p a then f a else g a
theorem Continuous.if {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} {p : αProp} [(a : α) → Decidable (p a)] (hp : afrontier {x : α | p x}, f a = g a) (hf : Continuous f) (hg : Continuous g) :
Continuous fun (a : α) => if p a then f a else g a
theorem continuous_if_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} (p : Prop) [Decidable p] (hf : pContinuous f) (hg : ¬pContinuous g) :
Continuous fun (a : α) => if p then f a else g a
theorem Continuous.if_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} (p : Prop) [Decidable p] (hf : Continuous f) (hg : Continuous g) :
Continuous fun (a : α) => if p then f a else g a
theorem continuous_piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} {s : Set α} [(a : α) → Decidable (a s)] (hs : afrontier s, f a = g a) (hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure s)) :
theorem Continuous.piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} {s : Set α} [(a : α) → Decidable (a s)] (hs : afrontier s, f a = g a) (hf : Continuous f) (hg : Continuous g) :
theorem IsOpen.ite' {α : Type u_1} [TopologicalSpace α] {s s' t : Set α} (hs : IsOpen s) (hs' : IsOpen s') (ht : xfrontier t, x s x s') :
IsOpen (t.ite s s')
theorem IsOpen.ite {α : Type u_1} [TopologicalSpace α] {s s' t : Set α} (hs : IsOpen s) (hs' : IsOpen s') (ht : s frontier t = s' frontier t) :
IsOpen (t.ite s s')
theorem ite_inter_closure_eq_of_inter_frontier_eq {α : Type u_1} [TopologicalSpace α] {s s' t : Set α} (ht : s frontier t = s' frontier t) :
t.ite s s' closure t = s closure t
theorem continuousOn_piecewise_ite' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} {s s' t : Set α} [(x : α) → Decidable (x t)] (h : ContinuousOn f (s closure t)) (h' : ContinuousOn g (s' closure t)) (H : s frontier t = s' frontier t) (Heq : Set.EqOn f g (s frontier t)) :
ContinuousOn (t.piecewise f g) (t.ite s s')
theorem continuousOn_piecewise_ite {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : αβ} {s s' t : Set α} [(x : α) → Decidable (x t)] (h : ContinuousOn f s) (h' : ContinuousOn g s') (H : s frontier t = s' frontier t) (Heq : Set.EqOn f g (s frontier t)) :
ContinuousOn (t.piecewise f g) (t.ite s s')