p q : ℚ
s t : Set ℚ
a✝ : FirstCountableTopology ℚ∞
⊢ False
p q : ℚ
s t : Set ℚ
⊢ ¬FirstCountableTopology ℚ∞
intro
no goals
p q : ℚ
s t : Set ℚ
a✝ : FirstCountableTopology ℚ∞
⊢ False
exact not_countably_generated_nhds_infty_opc inferInstance