α : Type ?u.14563
inst✝ : TopologicalSpace α
x : EReal
hx : ⊥ < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x
α : Type ?u.14563
inst✝ : TopologicalSpace α
⊢ HasBasis (𝓝 ⊥) (fun x => True) fun x => Iio ↑x
refine nhds_bot_basis.to_hasBasis (fun x hx => ?_) fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩
case intro.intro
α : Type ?u.14563
inst✝ : TopologicalSpace α
x : EReal
hx : ⊥ < x
y : ℚ
hxy : ↑↑y < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x
α : Type ?u.14563
inst✝ : TopologicalSpace α
x : EReal
hx : ⊥ < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x
rcases exists_rat_btwn_of_lt hx with ⟨y, -, hxy⟩
no goals
case intro.intro
α : Type ?u.14563
inst✝ : TopologicalSpace α
x : EReal
hx : ⊥ < x
y : ℚ
hxy : ↑↑y < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x
exact ⟨_, trivial, Iio_subset_Iio hxy.le⟩