p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
⊢ False
p q : ℚ
s t : Set ℚ
⊢ ¬IsCountablyGenerated (𝓝 ∞)
intro
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
this : IsCountablyGenerated (comap OnePoint.some (𝓝 ∞))
⊢ False
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
⊢ False
have : IsCountablyGenerated (comap (OnePoint.some : ℚ → ℚ∞) (𝓝 ∞)) := by infer_instance
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
this : IsCountablyGenerated (cocompact ℚ)
⊢ False
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
this : IsCountablyGenerated (comap OnePoint.some (𝓝 ∞))
⊢ False
rw [OnePoint.comap_coe_nhds_infty, coclosedCompact_eq_cocompact] at this
no goals
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
this : IsCountablyGenerated (cocompact ℚ)
⊢ False
exact not_countably_generated_cocompact this
no goals
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
⊢ IsCountablyGenerated (comap OnePoint.some (𝓝 ∞))
infer_instance