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 : α) [Filter.NeBot (nhdsWithin a (Set.Iio a))] :
∃ᶠ (x : α) in nhds a, x < a
theorem frequently_gt_nhds {α : Type u_1} [TopologicalSpace α] [Preorder α] (a : α) [Filter.NeBot (nhdsWithin a (Set.Ioi a))] :
∃ᶠ (x : α) in nhds a, a < x
theorem Filter.Eventually.exists_lt {α : Type u_1} [TopologicalSpace α] [Preorder α] {a : α} [Filter.NeBot (nhdsWithin a (Set.Iio a))] {p : αProp} (h : ∀ᶠ (x : α) in nhds a, p x) :
∃ b < a, p b
theorem Filter.Eventually.exists_gt {α : Type u_1} [TopologicalSpace α] [Preorder α] {a : α} [Filter.NeBot (nhdsWithin a (Set.Ioi a))] {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) :
Equations
  • =
theorem nhdsWithin_Iic_neBot {α : Type u_1} [TopologicalSpace α] [Preorder α] {a : α} {b : α} (H : a b) :
Equations
  • =
theorem IsAntichain.interior_eq_empty {α : Type u_1} [TopologicalSpace α] [Preorder α] [∀ (x : α), Filter.NeBot (nhdsWithin x (Set.Iio x))] {s : Set α} (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) :
theorem IsAntichain.interior_eq_empty' {α : Type u_1} [TopologicalSpace α] [Preorder α] [∀ (x : α), Filter.NeBot (nhdsWithin x (Set.Ioi x))] {s : Set α} (hs : IsAntichain (fun (x x_1 : α) => x x_1) 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 : αβ} :