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