Commit 2023-07-19 07:03 d31423ae

View on Github →

feat: +1 proof that Sorgenfrey plane is not normal (#5775)

Estimated changes

Modified Counterexamples/SorgenfreyLine.lean

added theorem Counterexample.SorgenfreyLine.cardinal_antidiagonal

modified theorem Counterexample.SorgenfreyLine.isClosed_of_subset_antidiagonal

added theorem Counterexample.SorgenfreyLine.isSeparable_antidiagonal

modified theorem Counterexample.SorgenfreyLine.nhds_basis_Ico

modified theorem Counterexample.SorgenfreyLine.not_normalSpace_prod

added theorem Counterexample.SorgenfreyLine.not_separableSpace_antidiagonal

added theorem Counterexample.SorgenfreyLine.not_separatedNhds_rat_irrational_antidiag

Modified Mathlib.lean

Modified Mathlib/Topology/ContinuousFunction/Basic.lean

added theorem ContinuousMap.injective_restrict

Created Mathlib/Topology/Separation/NotNormal.lean

added theorem IsClosed.mk_lt_continuum

added theorem IsClosed.not_normal_of_continuum_le_mk