Theorem exists_countable_generateFrom_Ioi_Iio

Modification history

2025-09-11 07:52
Mathlib/Topology/Order/Basic.lean
feat: the topology on WithTop is second countable (#29466)
Added exists_countable_generateFrom_Ioi_IioView on Github →