# 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