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 frequently_lt_nhds {α : Type u_1} [TopologicalSpace α] [Preorder α] (a : α) [(nhdsWithin a (Set.Iio a)).NeBot] : ∃ᶠ (x : α) in nhds a, x < a

theorem frequently_gt_nhds {α : Type u_1} [TopologicalSpace α] [Preorder α] (a : α) [(nhdsWithin a (Set.Ioi a)).NeBot] : ∃ᶠ (x : α) in nhds a, a < x

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 < b ∧ p b

theorem nhdsWithin_Ici_neBot {α : Type u_1} [TopologicalSpace α] [Preorder α] {a b : α} (H₂ : a ≤ b) : (nhdsWithin b (Set.Ici a)).NeBot

theorem nhdsWithin_Iic_neBot {α : Type u_1} [TopologicalSpace α] [Preorder α] {a b : α} (H₂ : b ≤ a) : (nhdsWithin b (Set.Iic a)).NeBot

instance nhdsLE_neBot {α : Type u_1} [TopologicalSpace α] [Preorder α] (a : α) : (nhdsWithin a (Set.Iic a)).NeBot

instance nhdsGE_neBot {α : Type u_1} [TopologicalSpace α] [Preorder α] (a : α) : (nhdsWithin a (Set.Ici a)).NeBot

theorem nhdsLT_le_nhdsNE {α : Type u_1} [TopologicalSpace α] [Preorder α] (a : α) : nhdsWithin a (Set.Iio a) ≤ nhdsWithin a {a}ᶜ

theorem nhdsGT_le_nhdsNE {α : 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) : interior 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) : interior 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 continuousWithinAt_inter_Ioi_iff_Ici {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PartialOrder α] [TopologicalSpace β] {a : α} {f : α → β} {s : Set α} : ContinuousWithinAt f (s ∩ Set.Ioi a) a ↔ ContinuousWithinAt f (s ∩ Set.Ici a) a

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

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

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

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

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

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

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

theorem nhdsWithinLT_sup_nhdsWithinGE {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {s : Set α} (a : α) : nhdsWithin a (s ∩ Set.Iio a) ⊔ nhdsWithin a (s ∩ Set.Ici a) = nhdsWithin a s

theorem nhdsWithinGT_sup_nhdsWithinLE {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {s : Set α} (a : α) : nhdsWithin a (s ∩ Set.Ioi a) ⊔ nhdsWithin a (s ∩ Set.Iic a) = nhdsWithin a s

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

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

theorem nhdsWithinLE_sup_nhdsWithinGT {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {s : Set α} (a : α) : nhdsWithin a (s ∩ Set.Iic a) ⊔ nhdsWithin a (s ∩ Set.Ioi a) = nhdsWithin a s

theorem nhdsWithinGE_sup_nhdsWithinLT {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {s : Set α} (a : α) : nhdsWithin a (s ∩ Set.Ici a) ⊔ nhdsWithin a (s ∩ Set.Iio a) = nhdsWithin a s

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

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

theorem nhdsWithinLT_sup_nhdsWithinGT {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {s : Set α} (a : α) : nhdsWithin a (s ∩ Set.Iio a) ⊔ nhdsWithin a (s ∩ Set.Ioi a) = nhdsWithin a (s \ {a})

theorem nhdsWithinGT_sup_nhdsWithinLT {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {s : Set α} (a : α) : nhdsWithin a (s ∩ Set.Ioi a) ⊔ nhdsWithin a (s ∩ Set.Iio a) = nhdsWithin a (s \ {a})

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

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

theorem nhdsWithin_uIoo_left_le_nhdsNE {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {a b : α} : nhdsWithin a (Set.uIoo a b) ≤ nhdsWithin a {a}ᶜ

theorem nhdsWithin_uIoo_right_le_nhdsNE {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {a b : α} : nhdsWithin b (Set.uIoo a b) ≤ nhdsWithin b {b}ᶜ

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

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

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