Commit 2023-02-02 07:22 fc375665

View on Github →

feat: port Topology.Separation (#1940)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Basic.lean

added theorem clusterPt_iff_not_disjoint

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/Inseparable.lean

added theorem specializes_iff_clusterPt

Created Mathlib/Topology/Separation.lean

added theorem Bornology.relativelyCompact.isBounded_iff

added def Bornology.relativelyCompact

added theorem Bornology.relativelyCompact_eq_inCompact

added theorem CofiniteTopology.continuous_of

added theorem CompactExhaustion.isClosed

added theorem ConnectedSpace.infinite

added theorem Continuous.closedEmbedding

added theorem Continuous.ext_on

added theorem Continuous.isClosedMap

added theorem Continuous.isOpen_mulSupport

added theorem Continuous.limUnder_eq

added theorem ContinuousAt.eventually_ne

added theorem Dense.diff_finite

added theorem Dense.diff_finset

added theorem Dense.diff_singleton

added theorem Embedding.t2Space

added theorem Embedding.t5Space

added theorem Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete

added theorem Filter.HasBasis.nhds_closure

added theorem Filter.Tendsto.eventually_ne

added theorem Filter.Tendsto.limUnder_eq

added theorem Filter.coclosedCompact_eq_cocompact

added theorem Filter.coclosedCompact_le_cofinite

added theorem Filter.limUnder_eq_iff

added theorem Function.LeftInverse.closedEmbedding

added theorem Function.LeftInverse.closed_range

added theorem Inseparable.eq

added theorem IsClosed.exists_closed_singleton

added theorem IsCompact.binary_compact_cover

added theorem IsCompact.finite_compact_cover

added theorem IsCompact.inter

added theorem IsCompact.isClosed

added theorem IsPreconnected.infinite_of_nontrivial

added theorem Ne.nhdsWithin_compl_singleton

added theorem Ne.nhdsWithin_diff_singleton

added theorem PreconnectedSpace.trivial_of_discrete

added theorem RegularSpace.inf

added theorem RegularSpace.ofBasis

added theorem RegularSpace.ofExistsMemNhdsIsClosedSubset

added theorem RegularSpace.ofLift'_closure

added theorem SeparatedNhds.comm

added theorem SeparatedNhds.disjoint_closure_left

added theorem SeparatedNhds.disjoint_closure_right

added theorem SeparatedNhds.empty_left

added theorem SeparatedNhds.empty_right

added theorem SeparatedNhds.mono

added theorem SeparatedNhds.preimage

added theorem SeparatedNhds.symm

added theorem SeparatedNhds.union_left

added theorem SeparatedNhds.union_right

added def SeparatedNhds

added theorem Set.EqOn.of_subset_closure

added theorem Set.Finite.t2_separation

added theorem Set.Subsingleton.closure

added theorem Specializes.eq

added theorem T0Space.of_cover

added theorem T0Space.of_open_cover

added theorem TopologicalSpace.IsTopologicalBasis.exists_closure_subset

added theorem TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne

added theorem TopologicalSpace.IsTopologicalBasis.nhds_basis_closure

added theorem TopologicalSpace.subset_trans

added theorem Ultrafilter.lim_eq_iff_le_nhds

added theorem binterᵢ_basis_nhds

added theorem closed_nhds_basis

added theorem closure_singleton

added theorem compact_exists_clopen_in_open

added theorem compact_t2_tot_disc_iff_tot_sep

added theorem compl_singleton_mem_nhds

added theorem compl_singleton_mem_nhdsSet_iff

added theorem compl_singleton_mem_nhds_iff

added theorem connectedComponent_eq_interᵢ_clopen

added theorem continuousAt_of_tendsto_nhds

added theorem continuousAt_update_of_ne

added theorem continuousOn_update_iff

added theorem continuousWithinAt_update_of_ne

added theorem discrete_of_t1_of_finite

added theorem disjoint_lift'_closure_nhds

added theorem disjoint_nested_nhds

added theorem disjoint_nhdsSet_nhds

added theorem disjoint_nhdsWithin_of_mem_discrete

added theorem disjoint_nhds_nhds

added theorem disjoint_nhds_nhdsSet

added theorem disjoint_nhds_nhds_iff_not_specializes

added theorem disjoint_nhds_pure

added theorem disjoint_pure_nhds

added theorem eqOn_closure₂'

added theorem eqOn_closure₂

added theorem eq_of_nhds_neBot

added theorem eq_of_tendsto_nhds

added theorem exists_compact_superset_iff

added theorem exists_isOpen_xor'_mem

added theorem exists_mem_nhds_isClosed_subset

added theorem exists_nhds_disjoint_closure

added theorem exists_open_between_and_isCompact_closure

added theorem exists_open_nhds_disjoint_closure

added theorem exists_open_singleton_of_finite

added theorem exists_open_singleton_of_open_finite

added theorem exists_open_superset_and_isCompact_closure

added theorem exists_open_with_compact_closure

added theorem exists_subset_nhds_of_isCompact

added theorem finset_disjoint_finset_opens_of_t2

added theorem hasBasis_nhds_closure

added theorem hasBasis_opens_closure

added theorem image_closure_of_isCompact

added theorem infinite_of_mem_nhds

added theorem injective_nhdsSet

added theorem inseparable_eq_eq

added theorem inseparable_iff_eq

added theorem insert_mem_nhdsWithin_of_subset_insert

added theorem isClosedMap_const

added theorem isClosed_diagonal

added theorem isClosed_eq

added theorem isClosed_setOf_inseparable

added theorem isClosed_setOf_specializes

added theorem isClosed_singleton

added theorem isCompact_closure_of_subset_compact

added theorem isCompact_isCompact_separated

added theorem isIrreducible_iff_singleton

added theorem isOpen_compl_singleton

added theorem isOpen_iff_ultrafilter'

added theorem isOpen_ne

added theorem isOpen_ne_fun

added theorem isOpen_setOf_disjoint_nhds_nhds

added theorem isOpen_setOf_eventually_nhdsWithin

added theorem isOpen_singleton_of_finite_mem_nhds

added theorem isPreirreducible_iff_subsingleton

added theorem isTopologicalBasis_clopen

added theorem lift'_nhds_closure

added theorem limUnder_nhdsWithin_id

added theorem limUnder_nhds_id

added theorem lim_eq

added theorem lim_eq_iff

added theorem lim_nhds

added theorem lim_nhdsWithin

added theorem loc_compact_Haus_tot_disc_of_zero_dim

added theorem loc_compact_t2_tot_disc_iff_tot_sep

added theorem locally_compact_of_compact_nhds

added theorem minimal_nonempty_closed_eq_singleton

added theorem minimal_nonempty_closed_subsingleton

added theorem minimal_nonempty_open_eq_singleton

added theorem minimal_nonempty_open_subsingleton

added theorem nhdsSet_inj_iff

added theorem nhdsSet_le_iff

added theorem nhdsWithin_insert_of_ne

added theorem nhdsWithin_of_mem_discrete

added theorem nhds_basis_clopen

added theorem nhds_eq_nhds_iff

added theorem nhds_injective

added theorem nhds_inter_eq_singleton_of_mem_discrete

added theorem nhds_le_nhdsSet_iff

added theorem nhds_le_nhds_iff

added theorem normalOfCompactT2

added theorem normalSpaceOfT3SecondCountable

added theorem normal_exists_closure_subset

added theorem normal_separation

added theorem not_preirreducible_nontrivial_t2

added theorem pairwise_disjoint_nhds

added theorem point_disjoint_finset_opens_of_t2

added theorem pure_le_nhds_iff

added theorem regularSpace_TFAE

added theorem regularSpace_induced

added theorem regularSpace_infᵢ

added theorem regularSpace_infₛ

added theorem separatedNhds_iff_disjoint

added theorem separated_by_continuous

added theorem separated_by_openEmbedding

added theorem singleton_mem_nhdsWithin_of_mem_discrete

added def specializationOrder

added theorem specializes_comm

added theorem specializes_eq_eq

added theorem specializes_iff_eq

added theorem specializes_iff_inseparable

added theorem strictMono_nhdsSet

added theorem subsingleton_closure

added theorem t0Space_iff_exists_isOpen_xor'_mem

added theorem t0Space_iff_inseparable

added theorem t0Space_iff_nhds_injective

added theorem t0Space_iff_not_inseparable

added theorem t0Space_iff_or_not_mem_closure

added theorem t0Space_of_injective_of_continuous

added theorem t1Space_TFAE

added theorem t1Space_antitone

added theorem t1Space_iff_continuous_cofinite_of

added theorem t1Space_iff_disjoint_nhds_pure

added theorem t1Space_iff_disjoint_pure_nhds

added theorem t1Space_iff_exists_open

added theorem t1Space_iff_specializes_imp_eq

added theorem t1Space_of_injective_of_continuous

added theorem t2Space_iff_disjoint_nhds

added theorem t2Space_iff_nhds

added theorem t2_iff_isClosed_diagonal

added theorem t2_iff_nhds

added theorem t2_iff_ultrafilter

added theorem t2_separation

added theorem t2_separation_compact_nhds

added theorem t2_separation_nhds

added theorem tendsto_const_nhds_iff

added theorem tendsto_nhds_unique'

added theorem tendsto_nhds_unique

added theorem tendsto_nhds_unique_of_eventuallyEq

added theorem tendsto_nhds_unique_of_frequently_eq

added theorem totallySeparatedSpace_of_t1_of_basis_clopen