Theorem Counterexample.Omega1Space.not_normalSpace_shrink_Iio_prod_Iic_omega_one

Modification history

2026-09-09 03:44
Counterexamples/Omega1Space.lean
feat(Counterexamples): the space ω₁ (#41962) …
Added Counterexample.Omega1Space.not_normalSpace_shrink_Iio_prod_Iic_omega_oneView on Github →