Left and right continuity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

continuous_within_at_Ioi_iff_Ici: two definitions of right continuity (with (a, ∞) and with [a, ∞)) are equivalent;
continuous_within_at_Iio_iff_Iic: two definitions of left continuity (with (-∞, a) and with (-∞, a]) are equivalent;
continuous_at_iff_continuous_left_right, continuous_at_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 continuous_within_at_Ioi_iff_Ici {α : Type u_1} {β : Type u_2} [topological_space α] [partial_order α] [topological_space β] {a : α} {f : α → β} :

theorem continuous_within_at_Iio_iff_Iic {α : Type u_1} {β : Type u_2} [topological_space α] [partial_order α] [topological_space β] {a : α} {f : α → β} :

theorem nhds_left'_le_nhds_ne {α : Type u_1} [topological_space α] [partial_order α] (a : α) :

theorem nhds_right'_le_nhds_ne {α : Type u_1} [topological_space α] [partial_order α] (a : α) :

theorem nhds_left_sup_nhds_right {α : Type u_1} [topological_space α] [linear_order α] (a : α) :

theorem nhds_left'_sup_nhds_right {α : Type u_1} [topological_space α] [linear_order α] (a : α) :

theorem nhds_left_sup_nhds_right' {α : Type u_1} [topological_space α] [linear_order α] (a : α) :

theorem nhds_left'_sup_nhds_right' {α : Type u_1} [topological_space α] [linear_order α] (a : α) :

theorem continuous_at_iff_continuous_left_right {α : Type u_1} {β : Type u_2} [topological_space α] [linear_order α] [topological_space β] {a : α} {f : α → β} :

theorem continuous_at_iff_continuous_left'_right' {α : Type u_1} {β : Type u_2} [topological_space α] [linear_order α] [topological_space β] {a : α} {f : α → β} :