Documentation

Mathlib.Topology.Order.LeftRight

Left and right continuity #

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

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, p b
theorem nhdsWithin_Ici_neBot {α : Type u_1} [TopologicalSpace α] [Preorder α] {a : α} {b : α} (H₂ : a b) :
(nhdsWithin b (Set.Ici a)).NeBot
instance nhdsWithin_Ici_self_neBot {α : Type u_1} [TopologicalSpace α] [Preorder α] (a : α) :
(nhdsWithin a (Set.Ici a)).NeBot
Equations
  • =
theorem nhdsWithin_Iic_neBot {α : Type u_1} [TopologicalSpace α] [Preorder α] {a : α} {b : α} (H : a b) :
(nhdsWithin a (Set.Iic b)).NeBot
instance nhdsWithin_Iic_self_neBot {α : Type u_1} [TopologicalSpace α] [Preorder α] (a : α) :
(nhdsWithin a (Set.Iic a)).NeBot
Equations
  • =
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 : αβ} :
theorem continuousWithinAt_Iio_iff_Iic {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PartialOrder α] [TopologicalSpace β] {a : α} {f : αβ} :