# 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_Ioi {α : Type u_1} [] [] {a : α} :
@[simp]
theorem nhdsSet_Iio {α : Type u_1} [] [] {a : α} :
@[simp]
theorem nhdsSet_Ioo {α : Type u_1} [] [] {a : α} {b : α} :
theorem nhdsSet_Ici {α : Type u_1} [] [] {a : α} :
theorem nhdsSet_Iic {α : Type u_1} [] [] {a : α} :
theorem nhdsSet_Ico {α : Type u_1} [] [] {a : α} {b : α} (h : a < b) :
theorem nhdsSet_Ioc {α : Type u_1} [] [] {a : α} {b : α} (h : a < b) :
theorem nhdsSet_Icc {α : Type u_1} [] [] {a : α} {b : α} (h : a b) :

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

@[simp]
theorem Ioi_mem_nhdsSet_Ici_iff {α : Type u_1} [] [] {a : α} {b : α} :
nhdsSet () a < b
theorem Ioi_mem_nhdsSet_Ici {α : Type u_1} [] [] {a : α} {b : α} :
a < b nhdsSet ()

Alias of the reverse direction of Ioi_mem_nhdsSet_Ici_iff.

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

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

theorem Iio_mem_nhdsSet_Iic_iff {α : Type u_1} [] [] {a : α} {b : α} :
nhdsSet () a < b
theorem Iio_mem_nhdsSet_Iic {α : Type u_1} [] [] {a : α} {b : α} :
a < b nhdsSet ()

Alias of the reverse direction of Iio_mem_nhdsSet_Iic_iff.

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

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

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

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

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

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

theorem Ioi_mem_nhdsSet_Ioc {α : Type u_1} [] [] {a : α} {b : α} {c : α} (h : a b) :
theorem Iio_mem_nhdsSet_Ioc {α : Type u_1} [] [] {a : α} {b : α} {c : α} (h : b < c) :
theorem Ici_mem_nhdsSet_Ioc {α : Type u_1} [] [] {a : α} {b : α} {c : α} (h : a b) :
theorem Iic_mem_nhdsSet_Ioc {α : Type u_1} [] [] {a : α} {b : α} {c : α} (h : b < c) :
theorem Ioo_mem_nhdsSet_Ioc {α : Type u_1} [] [] {a : α} {b : α} {c : α} {d : α} (h : a b) (h' : c < d) :
theorem Icc_mem_nhdsSet_Ioc {α : Type u_1} [] [] {a : α} {b : α} {c : α} {d : α} (h : a b) (h' : c < d) :
theorem Ioc_mem_nhdsSet_Ioc {α : Type u_1} [] [] {a : α} {b : α} {c : α} {d : α} (h : a b) (h' : c < d) :
theorem Ico_mem_nhdsSet_Ioc {α : Type u_1} [] [] {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} [] [] [] (a : α) [h : Nonempty ()] :
(nhdsSet ()).HasBasis (fun (x : α) => a < x) Set.Iio
theorem hasBasis_nhdsSet_Iic_Iic {α : Type u_1} [] [] [] (a : α) [(nhdsWithin a ()).NeBot] :
(nhdsSet ()).HasBasis (fun (x : α) => a < x) Set.Iic
@[simp]
theorem Iic_mem_nhdsSet_Iic_iff {α : Type u_1} [] [] [] {a : α} {b : α} [(nhdsWithin b ()).NeBot] :
nhdsSet () b < a
theorem hasBasis_nhdsSet_Ici_Ioi {α : Type u_1} [] [] [] (a : α) [Nonempty ()] :
(nhdsSet ()).HasBasis (fun (x : α) => x < a) Set.Ioi
theorem hasBasis_nhdsSet_Ici_Ici {α : Type u_1} [] [] [] (a : α) [(nhdsWithin a ()).NeBot] :
(nhdsSet ()).HasBasis (fun (x : α) => x < a) Set.Ici
@[simp]
theorem Ici_mem_nhdsSet_Ici_iff {α : Type u_1} [] [] [] {a : α} {b : α} [(nhdsWithin b ()).NeBot] :
nhdsSet () a < b