Commit 2023-07-04 05:50 c60a13fa

View on Github →

feat: port Counterexamples.SorgenfreyLine (#4978)

Estimated changes

Modified Counterexamples.lean

Created Counterexamples/SorgenfreyLine.lean

added theorem Counterexample.SorgenfreyLine.continuous_toReal

added theorem Counterexample.SorgenfreyLine.denseRange_coe_rat

added theorem Counterexample.SorgenfreyLine.exists_Ico_disjoint_closed

added theorem Counterexample.SorgenfreyLine.isClopen_Ici

added theorem Counterexample.SorgenfreyLine.isClopen_Ici_prod

added theorem Counterexample.SorgenfreyLine.isClopen_Ico

added theorem Counterexample.SorgenfreyLine.isClopen_Iio

added theorem Counterexample.SorgenfreyLine.isClosed_antidiagonal

added theorem Counterexample.SorgenfreyLine.isClosed_iff

added theorem Counterexample.SorgenfreyLine.isClosed_of_subset_antidiagonal

added theorem Counterexample.SorgenfreyLine.isOpen_Ici

added theorem Counterexample.SorgenfreyLine.isOpen_Ico

added theorem Counterexample.SorgenfreyLine.isOpen_iff

added theorem Counterexample.SorgenfreyLine.map_toReal_nhds

added theorem Counterexample.SorgenfreyLine.nhds_antitone_basis_Ico_inv_pnat

added theorem Counterexample.SorgenfreyLine.nhds_basis_Ico

added theorem Counterexample.SorgenfreyLine.nhds_basis_Ico_inv_pnat

added theorem Counterexample.SorgenfreyLine.nhds_basis_Ico_rat

added theorem Counterexample.SorgenfreyLine.nhds_countable_basis_Ico_inv_pnat

added theorem Counterexample.SorgenfreyLine.nhds_eq_comap

added theorem Counterexample.SorgenfreyLine.nhds_eq_map

added theorem Counterexample.SorgenfreyLine.nhds_prod_antitone_basis_inv_pnat

added theorem Counterexample.SorgenfreyLine.not_metrizableSpace

added theorem Counterexample.SorgenfreyLine.not_normalSpace_prod

added theorem Counterexample.SorgenfreyLine.not_secondCountableTopology

added def Counterexample.SorgenfreyLine.toReal

added def Counterexample.SorgenfreyLine