no goals
α✝ : Type ?u.653000
β : Type ?u.653003
γ : Type ?u.653006
γ₂ : Type ?u.653009
δ : Type ?u.653012
ι : Sort y
s✝ t u : Set α✝
inst✝²² : TopologicalSpace α✝
inst✝²¹ : MeasurableSpace α✝
inst✝²⁰ : OpensMeasurableSpace α✝
inst✝¹⁹ : TopologicalSpace β
inst✝¹⁸ : MeasurableSpace β
inst✝¹⁷ : OpensMeasurableSpace β
inst✝¹⁶ : TopologicalSpace γ
inst✝¹⁵ : MeasurableSpace γ
inst✝¹⁴ : BorelSpace γ
inst✝¹³ : TopologicalSpace γ₂
inst✝¹² : MeasurableSpace γ₂
inst✝¹¹ : BorelSpace γ₂
inst✝¹⁰ : MeasurableSpace δ
α' : Type ?u.653105
inst✝⁹ : TopologicalSpace α'
inst✝⁸ : MeasurableSpace α'
inst✝⁷ : LinearOrder α✝
inst✝⁶ : OrderClosedTopology α✝
a b x : α✝
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : SecondCountableTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
s : Set α
hd : Dense s
⊢ ∀ (x : α), IsBot x → x ∈ s
simp