[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
⊢ 𝓝ˢ (Ici a) = 𝓝 a ⊔ 𝓟 (Ioi a)
[PROOFSTEP]
rw [← Ioi_insert, nhdsSet_insert, nhdsSet_Ioi]
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : a < b
⊢ 𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
[PROOFSTEP]
rw [← Ioo_insert_left h, nhdsSet_insert, nhdsSet_Ioo]
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : a < b
⊢ 𝓝ˢ (Ioc a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
[PROOFSTEP]
rw [← Ioo_insert_right h, nhdsSet_insert, nhdsSet_Ioo]
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : a ≤ b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
[PROOFSTEP]
rcases h.eq_or_lt with rfl | hlt
[GOAL]
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a c d : α
h : a ≤ a
⊢ 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : a ≤ b
hlt : a < b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
[PROOFSTEP]
rw [← Ioc_insert_left h, nhdsSet_insert, nhdsSet_Ioc hlt, sup_assoc]
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
⊢ Ioi a ∈ 𝓝ˢ (Ici b) ↔ a < b
[PROOFSTEP]
rw [isOpen_Ioi.mem_nhdsSet, Ici_subset_Ioi]
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : b ≤ c
⊢ Iio c ∈ 𝓝ˢ (Iio b)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : a ≤ b
⊢ Ioi a ∈ 𝓝ˢ (Ioi b)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
⊢ HasBasis (𝓝ˢ (Iic a)) (fun x => a < x) Iio
[PROOFSTEP]
refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨b, hab, hb⟩ ↦ mem_of_superset (Iio_mem_nhdsSet_Iic hab) hb⟩⟩
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝ˢ (Iic a)
⊢ ∃ i, a < i ∧ Iio i ⊆ s
[PROOFSTEP]
rw [nhdsSet_Iic, mem_sup, mem_principal] at hs 
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
⊢ ∃ i, a < i ∧ Iio i ⊆ s
[PROOFSTEP]
rcases exists_Ico_subset_of_mem_nhds hs.1 (Set.nonempty_coe_sort.1 h) with ⟨b, hab, hbs⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ i, a < i ∧ Iio i ⊆ s
[PROOFSTEP]
exact ⟨b, hab, Iio_subset_Iio_union_Ico.trans (union_subset hs.2 hbs)⟩
[GOAL]
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : NeBot (𝓝[Ioi a] a)
⊢ HasBasis (𝓝ˢ (Iic a)) (fun x => a < x) Iic
[PROOFSTEP]
have : Nonempty (Ioi a) := (Filter.nonempty_of_mem (self_mem_nhdsWithin : Ioi a ∈ 𝓝[>] a)).to_subtype
[GOAL]
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : NeBot (𝓝[Ioi a] a)
this : Nonempty ↑(Ioi a)
⊢ HasBasis (𝓝ˢ (Iic a)) (fun x => a < x) Iic
[PROOFSTEP]
refine (hasBasis_nhdsSet_Iic_Iio _).to_hasBasis (fun c hc ↦ ?_) (fun _ h ↦ ⟨_, h, Iio_subset_Iic_self⟩)
[GOAL]
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : NeBot (𝓝[Ioi a] a)
this : Nonempty ↑(Ioi a)
c : α
hc : a < c
⊢ ∃ i', a < i' ∧ Iic i' ⊆ Iio c
[PROOFSTEP]
simpa only [Iic_subset_Iio] using (Filter.nonempty_of_mem <| Ioo_mem_nhdsWithin_Ioi' hc)
