Commit 2023-02-13 08:36 b4c297bf

View on Github →

feat: port Topology.Alexandroff (#2229)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Alexandroff.lean

added theorem Alexandroff.coe_eq_coe

added theorem Alexandroff.coe_injective

added theorem Alexandroff.coe_ne_infty

added theorem Alexandroff.coe_preimage_infty

added theorem Alexandroff.comap_coe_nhds

added theorem Alexandroff.comap_coe_nhds_infty

added theorem Alexandroff.compl_image_coe

added theorem Alexandroff.compl_infty

added theorem Alexandroff.compl_range_coe

added theorem Alexandroff.continuousAt_coe

added theorem Alexandroff.continuousAt_infty'

added theorem Alexandroff.continuousAt_infty

added theorem Alexandroff.continuous_coe

added theorem Alexandroff.denseEmbedding_coe

added theorem Alexandroff.denseRange_coe

added theorem Alexandroff.hasBasis_nhds_infty

added def Alexandroff.infty

added theorem Alexandroff.infty_mem_opensOfCompl

added theorem Alexandroff.infty_ne_coe

added theorem Alexandroff.infty_not_mem_image_coe

added theorem Alexandroff.infty_not_mem_range_coe

added theorem Alexandroff.inseparable_coe

added theorem Alexandroff.inseparable_iff

added theorem Alexandroff.insert_infty_range_coe

added theorem Alexandroff.isClosed_iff_of_mem

added theorem Alexandroff.isClosed_iff_of_not_mem

added theorem Alexandroff.isClosed_image_coe

added theorem Alexandroff.isClosed_infty

added theorem Alexandroff.isCompl_range_coe_infty

added theorem Alexandroff.isOpenMap_coe

added theorem Alexandroff.isOpen_compl_image_coe

added theorem Alexandroff.isOpen_def

added theorem Alexandroff.isOpen_iff_of_mem'

added theorem Alexandroff.isOpen_iff_of_mem

added theorem Alexandroff.isOpen_iff_of_not_mem

added theorem Alexandroff.isOpen_image_coe

added theorem Alexandroff.isOpen_range_coe

added theorem Alexandroff.le_nhds_infty

added theorem Alexandroff.ne_infty_iff_exists

added theorem Alexandroff.nhdsWithin_coe

added theorem Alexandroff.nhdsWithin_coe_image

added theorem Alexandroff.nhdsWithin_compl_infty_eq

added theorem Alexandroff.nhds_coe_eq

added theorem Alexandroff.nhds_infty_eq

added theorem Alexandroff.not_continuous_cofiniteTopology_of_symm

added theorem Alexandroff.not_inseparable_coe_infty

added theorem Alexandroff.not_inseparable_infty_coe

added theorem Alexandroff.not_mem_range_coe_iff

added theorem Alexandroff.not_specializes_infty_coe

added theorem Alexandroff.openEmbedding_coe

added def Alexandroff.opensOfCompl

added theorem Alexandroff.range_coe_inter_infty

added theorem Alexandroff.range_coe_union_infty

added def Alexandroff.some

added theorem Alexandroff.specializes_coe

added theorem Alexandroff.tendsto_nhds_infty'

added theorem Alexandroff.tendsto_nhds_infty

added theorem Alexandroff.ultrafilter_le_nhds_infty

added def Alexandroff

added theorem Continuous.homeoOfEquivCompactToT2.t1_counterexample

Modified Mathlib/Topology/SubsetProperties.lean

added theorem disjoint_nhds_cocompact