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