case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[Iic a] a
hbs : Icc b a ⊆ s
⊢ ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
⊢ ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
rcases exists_Icc_mem_subset_of_mem_nhdsWithin_Iic (nhdsWithin_le_nhds hs) with
  ⟨b, hba, hb_nhds, hbs⟩
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[Iic a] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[Ici a] a
hcs : Icc a c ⊆ s
⊢ ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[Iic a] a
hbs : Icc b a ⊆ s
⊢ ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
rcases exists_Icc_mem_subset_of_mem_nhdsWithin_Ici (nhdsWithin_le_nhds hs) with
  ⟨c, hac, hc_nhds, hcs⟩
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[Iic a] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[Ici a] a
hcs : Icc a c ⊆ s
⊢ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[Iic a] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[Ici a] a
hcs : Icc a c ⊆ s
⊢ ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
refine' ⟨b, c, ⟨hba, hac⟩, _⟩
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[Iic a] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[Ici a] a
hcs : Icc a c ⊆ s
⊢ Icc b a ∪ Icc a c ∈ 𝓝[Iic a] a ⊔ 𝓝[Ici a] a ∧ Icc b a ∪ Icc a c ⊆ s
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[Iic a] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[Ici a] a
hcs : Icc a c ⊆ s
⊢ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
rw [← Icc_union_Icc_eq_Icc hba hac, ← nhds_left_sup_nhds_right]
no goals
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[Iic a] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[Ici a] a
hcs : Icc a c ⊆ s
⊢ Icc b a ∪ Icc a c ∈ 𝓝[Iic a] a ⊔ 𝓝[Ici a] a ∧ Icc b a ∪ Icc a c ⊆ s
exact ⟨union_mem_sup hb_nhds hc_nhds, union_subset hbs hcs⟩