α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x z : α
hz : z ∈ Ioi x
⊢ z ∈ ⋃ (y : α) (_ : y ∈ s ∩ Ioi x), Ioi y
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x : α
⊢ Ioi x = ⋃ (y : α) (_ : y ∈ s ∩ Ioi x), Ioi y
refine Subset.antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun y hy ↦ Ioi_subset_Ioi (le_of_lt hy.2))
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x z : α
hz : z ∈ Ioi x
y : α
hys : y ∈ s
hxy : x < y
hyz : y < z
⊢ z ∈ ⋃ (y : α) (_ : y ∈ s ∩ Ioi x), Ioi y
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x z : α
hz : z ∈ Ioi x
⊢ z ∈ ⋃ (y : α) (_ : y ∈ s ∩ Ioi x), Ioi y
rcases hs.exists_between hz with ⟨y, hys, hxy, hyz⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x z : α
hz : z ∈ Ioi x
y : α
hys : y ∈ s
hxy : x < y
hyz : y < z
⊢ z ∈ ⋃ (y : α) (_ : y ∈ s ∩ Ioi x), Ioi y
exact mem_iUnion₂.2 ⟨y, ⟨hys, hxy⟩, hyz⟩