α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c, c ∈ s ∧ a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
⊢ Set.Nonempty (U ∩ s)
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c, c ∈ s ∧ a < c ∧ c < b
⊢ Dense s
refine dense_iff_inter_open.2 fun U U_open U_nonempty => ?_
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c, c ∈ s ∧ a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
a b : α
hab : a < b
H : Ioo a b ⊆ U
⊢ Set.Nonempty (U ∩ s)
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c, c ∈ s ∧ a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
⊢ Set.Nonempty (U ∩ s)
obtain ⟨a, b, hab, H⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ U := U_open.exists_Ioo_subset U_nonempty
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c, c ∈ s ∧ a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
a b : α
hab : a < b
H : Ioo a b ⊆ U
x : α
xs : x ∈ s
hx : a < x ∧ x < b
⊢ Set.Nonempty (U ∩ s)
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c, c ∈ s ∧ a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
a b : α
hab : a < b
H : Ioo a b ⊆ U
⊢ Set.Nonempty (U ∩ s)
obtain ⟨x, xs, hx⟩ : ∃ x ∈ s, a < x ∧ x < b := h hab
no goals
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c, c ∈ s ∧ a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
a b : α
hab : a < b
H : Ioo a b ⊆ U
x : α
xs : x ∈ s
hx : a < x ∧ x < b
⊢ Set.Nonempty (U ∩ s)
exact ⟨x, ⟨H hx, xs⟩⟩