no goals
α : Type u
β : Type v
γ : Type w
⊢ ∀ (u : Set ℝ), (u ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) → IsOpen u
simp (config := { contextual := true }) [isOpen_Ioo]
α : Type u
β : Type v
γ : Type w
a : ℝ
v : Set ℝ
hav : a ∈ v
hv : IsOpen v
l u : ℝ
hl : l < a
hu : a < u
h : Ioo l u ⊆ v
q : ℚ
hlq : l < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < u
⊢ ∃ i i_1 i_2, Ioo ↑q ↑p ∈ {Ioo ↑i ↑i_1}
α : Type u
β : Type v
γ : Type w
a : ℝ
v : Set ℝ
hav : a ∈ v
hv : IsOpen v
l u : ℝ
hl : l < a
hu : a < u
h : Ioo l u ⊆ v
q : ℚ
hlq : l < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < u
⊢ Ioo ↑q ↑p ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}
simp only [mem_iUnion]
no goals
α : Type u
β : Type v
γ : Type w
a : ℝ
v : Set ℝ
hav : a ∈ v
hv : IsOpen v
l u : ℝ
hl : l < a
hu : a < u
h : Ioo l u ⊆ v
q : ℚ
hlq : l < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < u
⊢ ∃ i i_1 i_2, Ioo ↑q ↑p ∈ {Ioo ↑i ↑i_1}
exact ⟨q, p, Rat.cast_lt.1 <| hqa.trans hap, rfl⟩