α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s) ↔ ∃ u, a < u ∧ Icc a u ⊆ s
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[Ici a] a ↔ ∃ u, a < u ∧ Icc a u ⊆ s
rw [mem_nhdsWithin_Ici_iff_exists_Ico_subset]
case mp
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s) → ∃ u, a < u ∧ Icc a u ⊆ s

case mpr
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, a < u ∧ Icc a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s) ↔ ∃ u, a < u ∧ Icc a u ⊆ s
constructor
case mp.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ico a u ⊆ s
⊢ ∃ u, a < u ∧ Icc a u ⊆ s
case mp
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s) → ∃ u, a < u ∧ Icc a u ⊆ s
rintro ⟨u, au, as⟩
case mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ico a u ⊆ s
v : α
hv : a < v ∧ v < u
⊢ ∃ u, a < u ∧ Icc a u ⊆ s
case mp.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ico a u ⊆ s
⊢ ∃ u, a < u ∧ Icc a u ⊆ s
rcases exists_between au with ⟨v, hv⟩
no goals
case mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ico a u ⊆ s
v : α
hv : a < v ∧ v < u
⊢ ∃ u, a < u ∧ Icc a u ⊆ s
exact ⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
u : α
au : a < u
as : Icc a u ⊆ s
⊢ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
case mpr
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, a < u ∧ Icc a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
rintro ⟨u, au, as⟩
no goals
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
u : α
au : a < u
as : Icc a u ⊆ s
⊢ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
exact ⟨u, au, Subset.trans Ico_subset_Icc_self as⟩