Documentation

Mathlib.Topology.Order.NhdsSet

Set neighborhoods of intervals #

In this file we prove basic theorems about 𝓝ˢ s, where s is one of the intervals Set.Ici, Set.Iic, Set.Ioi, Set.Iio, Set.Ico, Set.Ioc, Set.Ioo, and Set.Icc.

First, we prove lemmas in terms of filter equalities. Then we prove lemmas about s ∈ 𝓝ˢ t, where both s and t are intervals. Finally, we prove a few lemmas about filter bases of 𝓝ˢ (Iic a) and 𝓝ˢ (Ici a).

Formulae for 𝓝ˢ of intervals #

@[simp]
theorem nhdsSet_Ioo {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} :
theorem nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
theorem nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
theorem nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} (h : a b) :

Lemmas about Ixi _ ∈ 𝓝ˢ (Set.Ici _) #

@[simp]
theorem Ioi_mem_nhdsSet_Ici_iff {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} :
theorem Ioi_mem_nhdsSet_Ici {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} :
a < bSet.Ioi a nhdsSet (Set.Ici b)

Alias of the reverse direction of Ioi_mem_nhdsSet_Ici_iff.

theorem Ici_mem_nhdsSet_Ici {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :

Lemmas about Iix _ ∈ 𝓝ˢ (Set.Iic _) #

theorem Iio_mem_nhdsSet_Iic_iff {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} :
theorem Iio_mem_nhdsSet_Iic {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} :
a < bSet.Iio b nhdsSet (Set.Iic a)

Alias of the reverse direction of Iio_mem_nhdsSet_Iic_iff.

theorem Iic_mem_nhdsSet_Iic {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :

Lemmas about Ixx _ ?_ ∈ 𝓝ˢ (Set.Icc _ _) #

theorem Ioi_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a < b) :
theorem Ici_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a < b) :
theorem Iio_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b < c) :
theorem Iic_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b < c) :
theorem Ioo_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c < d) :
theorem Ico_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c < d) :
theorem Ioc_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c < d) :
theorem Icc_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c < d) :

Lemmas about Ixx _ ?_ ∈ 𝓝ˢ (Set.Ico _ _) #

theorem Ici_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a < b) :
theorem Ioi_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a < b) :
theorem Iio_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b c) :
theorem Iic_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b c) :
theorem Ioo_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c d) :
theorem Icc_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c d) :
theorem Ioc_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c d) :
theorem Ico_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c d) :

Lemmas about Ixx _ ?_ ∈ 𝓝ˢ (Set.Ioc _ _) #

theorem Ioi_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a b) :
theorem Iio_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b < c) :
theorem Ici_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a b) :
theorem Iic_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b < c) :
theorem Ioo_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a b) (h' : c < d) :
theorem Icc_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a b) (h' : c < d) :
theorem Ioc_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a b) (h' : c < d) :
theorem Ico_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a b) (h' : c < d) :

Filter bases of 𝓝ˢ (Iic a) and 𝓝ˢ (Ici a) #

theorem hasBasis_nhdsSet_Iic_Iio {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] (a : α) [h : Nonempty (Set.Ioi a)] :
(nhdsSet (Set.Iic a)).HasBasis (fun (x : α) => a < x) Set.Iio
theorem hasBasis_nhdsSet_Iic_Iic {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] (a : α) [(nhdsWithin a (Set.Ioi a)).NeBot] :
(nhdsSet (Set.Iic a)).HasBasis (fun (x : α) => a < x) Set.Iic
@[simp]
theorem Iic_mem_nhdsSet_Iic_iff {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {a : α} {b : α} [(nhdsWithin b (Set.Ioi b)).NeBot] :
theorem hasBasis_nhdsSet_Ici_Ioi {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] (a : α) [Nonempty (Set.Iio a)] :
(nhdsSet (Set.Ici a)).HasBasis (fun (x : α) => x < a) Set.Ioi
theorem hasBasis_nhdsSet_Ici_Ici {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] (a : α) [(nhdsWithin a (Set.Iio a)).NeBot] :
(nhdsSet (Set.Ici a)).HasBasis (fun (x : α) => x < a) Set.Ici
@[simp]
theorem Ici_mem_nhdsSet_Ici_iff {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {a : α} {b : α} [(nhdsWithin b (Set.Iio b)).NeBot] :