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 #

source
@[simp]
theorem nhdsSet_Ioi {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} :
nhdsSet (Set.Ioi a) = Filter.principal (Set.Ioi a)
source
@[simp]
theorem nhdsSet_Iio {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} :
nhdsSet (Set.Iio a) = Filter.principal (Set.Iio a)
source
@[simp]
theorem nhdsSet_Ioo {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} :
nhdsSet (Set.Ioo a b) = Filter.principal (Set.Ioo a b)
source
theorem nhdsSet_Ici {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} :
nhdsSet (Set.Ici a) = nhds a ⊔ Filter.principal (Set.Ioi a)
source
theorem nhdsSet_Iic {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} :
nhdsSet (Set.Iic a) = nhds a ⊔ Filter.principal (Set.Iio a)
source
theorem nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
nhdsSet (Set.Ico a b) = nhds a ⊔ Filter.principal (Set.Ioo a b)
source
theorem nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
nhdsSet (Set.Ioc a b) = nhds b ⊔ Filter.principal (Set.Ioo a b)
source
theorem nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} (h : a ≤ b) :
nhdsSet (Set.Icc a b) = nhds a ⊔ nhds b ⊔ Filter.principal (Set.Ioo a b)

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

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

Alias of the reverse direction of Ioi_mem_nhdsSet_Ici_iff.

source
theorem Ici_mem_nhdsSet_Ici {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
Set.Ici a ∈ nhdsSet (Set.Ici b)

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

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

Alias of the reverse direction of Iio_mem_nhdsSet_Iic_iff.

source
theorem Iic_mem_nhdsSet_Iic {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
Set.Iic b ∈ nhdsSet (Set.Iic a)

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

source
theorem Ioi_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a < b) :
Set.Ioi a ∈ nhdsSet (Set.Icc b c)
source
theorem Ici_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a < b) :
Set.Ici a ∈ nhdsSet (Set.Icc b c)
source
theorem Iio_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b < c) :
Set.Iio c ∈ nhdsSet (Set.Icc a b)
source
theorem Iic_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b < c) :
Set.Iic c ∈ nhdsSet (Set.Icc a b)
source
theorem Ioo_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c < d) :
Set.Ioo a d ∈ nhdsSet (Set.Icc b c)
source
theorem Ico_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c < d) :
Set.Ico a d ∈ nhdsSet (Set.Icc b c)
source
theorem Ioc_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c < d) :
Set.Ioc a d ∈ nhdsSet (Set.Icc b c)
source
theorem Icc_mem_nhdsSet_Icc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c < d) :
Set.Icc a d ∈ nhdsSet (Set.Icc b c)

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

source
theorem Ici_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a < b) :
Set.Ici a ∈ nhdsSet (Set.Ico b c)
source
theorem Ioi_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a < b) :
Set.Ioi a ∈ nhdsSet (Set.Ico b c)
source
theorem Iio_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b ≤ c) :
Set.Iio c ∈ nhdsSet (Set.Ico a b)
source
theorem Iic_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b ≤ c) :
Set.Iic c ∈ nhdsSet (Set.Ico a b)
source
theorem Ioo_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c ≤ d) :
Set.Ioo a d ∈ nhdsSet (Set.Ico b c)
source
theorem Icc_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c ≤ d) :
Set.Icc a d ∈ nhdsSet (Set.Ico b c)
source
theorem Ioc_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c ≤ d) :
Set.Ioc a d ∈ nhdsSet (Set.Ico b c)
source
theorem Ico_mem_nhdsSet_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a < b) (h' : c ≤ d) :
Set.Ico a d ∈ nhdsSet (Set.Ico b c)

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

source
theorem Ioi_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a ≤ b) :
Set.Ioi a ∈ nhdsSet (Set.Ioc b c)
source
theorem Iio_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b < c) :
Set.Iio c ∈ nhdsSet (Set.Ioc a b)
source
theorem Ici_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : a ≤ b) :
Set.Ici a ∈ nhdsSet (Set.Ioc b c)
source
theorem Iic_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (h : b < c) :
Set.Iic c ∈ nhdsSet (Set.Ioc a b)
source
theorem Ioo_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a ≤ b) (h' : c < d) :
Set.Ioo a d ∈ nhdsSet (Set.Ioc b c)
source
theorem Icc_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a ≤ b) (h' : c < d) :
Set.Icc a d ∈ nhdsSet (Set.Ioc b c)
source
theorem Ioc_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a ≤ b) (h' : c < d) :
Set.Ioc a d ∈ nhdsSet (Set.Ioc b c)
source
theorem Ico_mem_nhdsSet_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {a : α} {b : α} {c : α} {d : α} (h : a ≤ b) (h' : c < d) :
Set.Ico a d ∈ nhdsSet (Set.Ioc b c)

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

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