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 ata
if and only if it is left and right continuous ata
.
Tags #
left continuous, right continuous
theorem
frequently_lt_nhds
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
(a : α)
[(nhdsWithin a (Set.Iio a)).NeBot]
:
theorem
frequently_gt_nhds
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
(a : α)
[(nhdsWithin a (Set.Ioi a)).NeBot]
:
theorem
Filter.Eventually.exists_lt
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
{a : α}
[(nhdsWithin a (Set.Iio a)).NeBot]
{p : α → Prop}
(h : ∀ᶠ (x : α) in nhds a, p x)
:
∃ b < a, p b
theorem
Filter.Eventually.exists_gt
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
{a : α}
[(nhdsWithin a (Set.Ioi a)).NeBot]
{p : α → Prop}
(h : ∀ᶠ (x : α) in nhds a, p x)
:
∃ b > a, p b
theorem
nhdsWithin_Ici_neBot
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
{a b : α}
(H₂ : a ≤ b)
:
(nhdsWithin b (Set.Ici a)).NeBot
theorem
nhdsWithin_Ici_self_neBot
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
(a : α)
:
(nhdsWithin a (Set.Ici a)).NeBot
theorem
nhdsWithin_Iic_neBot
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
{a b : α}
(H : a ≤ b)
:
(nhdsWithin a (Set.Iic b)).NeBot
theorem
nhdsWithin_Iic_self_neBot
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
(a : α)
:
(nhdsWithin a (Set.Iic a)).NeBot
theorem
nhds_left'_le_nhds_ne
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
(a : α)
:
nhdsWithin a (Set.Iio a) ≤ nhdsWithin a {a}ᶜ
theorem
nhds_right'_le_nhds_ne
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
(a : α)
:
nhdsWithin a (Set.Ioi a) ≤ nhdsWithin a {a}ᶜ
theorem
IsAntichain.interior_eq_empty
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
[∀ (x : α), (nhdsWithin x (Set.Iio x)).NeBot]
{s : Set α}
(hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s)
:
theorem
IsAntichain.interior_eq_empty'
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
[∀ (x : α), (nhdsWithin x (Set.Ioi x)).NeBot]
{s : Set α}
(hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s)
:
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_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
nhdsWithin_right_sup_nhds_singleton
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
(a : α)
:
nhdsWithin a (Set.Ioi a) ⊔ nhdsWithin a {a} = nhdsWithin a (Set.Ici 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