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 :
∀ a ∈ s ∩ frontier {a : α | p a},
Filter.Tendsto f (nhdsWithin a (s ∩ {a : α | p a})) (nhds (if p a then f a else g a)))
(hpg :
∀ a ∈ s ∩ 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 : ∀ a ∈ s ∩ frontier t, Filter.Tendsto f (nhdsWithin a (s ∩ t)) (nhds (t.piecewise f g a)))
(hpg : ∀ a ∈ s ∩ 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ᶜ))
:
ContinuousOn (t.piecewise f g) s
theorem
ContinuousOn.if
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f g : α → β}
{s : Set α}
{p : α → Prop}
[(a : α) → Decidable (p a)]
(hp : ∀ a ∈ s ∩ 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 : ∀ a ∈ s ∩ frontier t, f a = g a)
(hf : ContinuousOn f (s ∩ closure t))
(hg : ContinuousOn g (s ∩ closure tᶜ))
:
ContinuousOn (t.piecewise f g) s
theorem
continuous_if'
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f g : α → β}
{p : α → Prop}
[(a : α) → Decidable (p a)]
(hpf : ∀ a ∈ frontier {x : α | p x}, Filter.Tendsto f (nhdsWithin a {x : α | p x}) (nhds (if p a then f a else g a)))
(hpg : ∀ a ∈ frontier {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 : ∀ a ∈ frontier {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 : ∀ a ∈ frontier {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 : p → Continuous f)
(hg : ¬p → Continuous 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 : ∀ a ∈ frontier s, f a = g a)
(hf : ContinuousOn f (closure s))
(hg : ContinuousOn g (closure sᶜ))
:
Continuous (s.piecewise f g)
theorem
Continuous.piecewise
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f g : α → β}
{s : Set α}
[(a : α) → Decidable (a ∈ s)]
(hs : ∀ a ∈ frontier s, f a = g a)
(hf : Continuous f)
(hg : Continuous g)
:
Continuous (s.piecewise f g)
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')