case mp
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a → ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s
constructor
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
h : s ∈ 𝓝 a
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a → ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s
intro h
case mp.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
h : s ∈ 𝓝 a
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s
rcases exists_Ico_subset_of_mem_nhds h hu with ⟨u, au, hu⟩
case mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl✝ : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
l : α
la : l < a
hl : Ioc l a ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s
case mp.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s
rcases exists_Ioc_subset_of_mem_nhds h hl with ⟨l, la, hl⟩
no goals
case mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl✝ : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
l : α
la : l < a
hl : Ioc l a ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s
exact ⟨l, u, ⟨la, au⟩, Ioc_union_Ico_eq_Ioo la au ▸ union_subset hl hu⟩
case mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
l u : α
ha : a ∈ Ioo l u
h : Ioo l u ⊆ s
⊢ s ∈ 𝓝 a
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a
rintro ⟨l, u, ha, h⟩
no goals
case mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
l u : α
ha : a ∈ Ioo l u
h : Ioo l u ⊆ s
⊢ s ∈ 𝓝 a
apply mem_of_superset (Ioo_mem_nhds ha.1 ha.2) h