Left and right continuity

In this file we prove a few lemmas about left and right continuous functions:

• continuousWithinAt_Ioi_iff_Ici: two definitions of right continuity (with (a, ∞) and with [a, ∞)) are equivalent;
• continuousWithinAt_Iio_iff_Iic: two definitions of left continuity (with (-∞, a) and with (-∞, a]) are equivalent;
• continuousAt_iff_continuous_left_right, continuousAt_iff_continuous_left'_right' : a function is continuous at a if and only if it is left and right continuous at a.

Tags

left continuous, right continuous

theorem continuousWithinAt_Ioi_iff_Ici {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PartialOrder α] [TopologicalSpace β] {a : α} {f : α → β} : ContinuousWithinAt f (Set.Ioi a) a ↔ ContinuousWithinAt f (Set.Ici a) a

theorem continuousWithinAt_Iio_iff_Iic {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PartialOrder α] [TopologicalSpace β] {a : α} {f : α → β} : ContinuousWithinAt f (Set.Iio a) a ↔ ContinuousWithinAt f (Set.Iic a) a

theorem nhds_left'_le_nhds_ne {α : Type u_1} [TopologicalSpace α] [PartialOrder α] (a : α) : nhdsWithin a (Set.Iio a) ≤ nhdsWithin a {a}ᶜ

theorem nhds_right'_le_nhds_ne {α : Type u_1} [TopologicalSpace α] [PartialOrder α] (a : α) : nhdsWithin a (Set.Ioi a) ≤ nhdsWithin a {a}ᶜ

theorem nhds_left_sup_nhds_right {α : Type u_1} [TopologicalSpace α] [LinearOrder α] (a : α) : nhdsWithin a (Set.Iic a) ⊔ nhdsWithin a (Set.Ici a) = nhds a

theorem nhds_left'_sup_nhds_right {α : Type u_1} [TopologicalSpace α] [LinearOrder α] (a : α) : nhdsWithin a (Set.Iio a) ⊔ nhdsWithin a (Set.Ici a) = nhds a

theorem nhds_left_sup_nhds_right' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] (a : α) : nhdsWithin a (Set.Iic a) ⊔ nhdsWithin a (Set.Ioi a) = nhds a

theorem nhds_left'_sup_nhds_right' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] (a : α) : nhdsWithin a (Set.Iio a) ⊔ nhdsWithin a (Set.Ioi a) = nhdsWithin a {a}ᶜ

theorem continuousAt_iff_continuous_left_right {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrder α] [TopologicalSpace β] {a : α} {f : α → β} : ContinuousAt f a ↔ ContinuousWithinAt f (Set.Iic a) a ∧ ContinuousWithinAt f (Set.Ici a) a

theorem continuousAt_iff_continuous_left'_right' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrder α] [TopologicalSpace β] {a : α} {f : α → β} : ContinuousAt f a ↔ ContinuousWithinAt f (Set.Iio a) a ∧ ContinuousWithinAt f (Set.Ioi a) a