Commit 2025-04-08 01:10 54601c47

View on Github →

chore: split Topology.Basic (#23717)

Topology.Basic is now focused on the IsOpen/IsClosed predicates.
Topology.Closure contains lemmas about the functions interior/closure/frontier.
Topology.Neighborhoods contains lemmas about neighborhoods in a topology.
Topology.ClusterPt contains lemmas about cluster and accumulation points.
Topology.Continuous deals with continuity and continuous functions.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/Padics/Hensel.lean

Modified Mathlib/Topology/Algebra/Algebra.lean

Modified Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

Modified Mathlib/Topology/Basic.lean

deleted theorem AccPt.clusterPt

deleted theorem AccPt.mono

deleted theorem ClusterPt.frequently

deleted theorem ClusterPt.map

deleted theorem ClusterPt.mono

deleted theorem ClusterPt.neBot

deleted theorem ClusterPt.of_inf_left

deleted theorem ClusterPt.of_inf_right

deleted theorem ClusterPt.of_le_nhds'

deleted theorem ClusterPt.of_le_nhds

deleted theorem ClusterPt.of_nhds_le

deleted theorem Continuous.closure_preimage_subset

deleted theorem Continuous.comp'

deleted theorem Continuous.comp

deleted theorem Continuous.congr

deleted theorem Continuous.continuousAt

deleted theorem Continuous.frontier_preimage_subset

deleted theorem Continuous.iterate

deleted theorem Continuous.range_subset_closure_image_dense

deleted theorem Continuous.tendsto'

deleted theorem Continuous.tendsto

deleted theorem ContinuousAt.comp'

deleted theorem ContinuousAt.comp_of_eq

deleted theorem ContinuousAt.congr

deleted theorem ContinuousAt.eventually_mem

deleted theorem ContinuousAt.iterate

deleted theorem ContinuousAt.preimage_mem_nhds

deleted theorem ContinuousAt.tendsto

deleted theorem Dense.denseRange_val

deleted theorem Dense.exists_mem_open

deleted theorem Dense.induction

deleted theorem Dense.inter_nhds_nonempty

deleted theorem Dense.inter_of_isOpen_left

deleted theorem Dense.inter_of_isOpen_right

deleted theorem Dense.interior_compl

deleted theorem Dense.mono

deleted theorem Dense.nonempty

deleted theorem Dense.nonempty_iff

deleted theorem Dense.open_subset_closure_inter

deleted theorem DenseRange.closure_range

deleted theorem DenseRange.comp

deleted theorem DenseRange.dense_image

deleted theorem DenseRange.dense_of_mapsTo

deleted theorem DenseRange.mem_nhds

deleted theorem DenseRange.nonempty

deleted def DenseRange.some

deleted theorem DenseRange.subset_closure_image_preimage_of_isOpen

deleted theorem Disjoint.closure_left

deleted theorem Disjoint.closure_right

deleted theorem Disjoint.frontier_left

deleted theorem Disjoint.frontier_right

deleted theorem Equiv.continuous_symm_iff

deleted theorem Equiv.isOpenMap_symm_iff

deleted theorem Filter.Eventually.eventually_nhds

deleted theorem Filter.Eventually.self_of_nhds

deleted theorem Filter.EventuallyEq.continuousAt

deleted theorem Filter.EventuallyEq.eq_of_nhds

deleted theorem Filter.EventuallyEq.eventuallyEq_nhds

deleted theorem Filter.EventuallyEq.mapClusterPt_iff

deleted theorem Filter.EventuallyEq.tendsto

deleted theorem Filter.EventuallyLE.eventuallyLE_nhds

deleted theorem Filter.Frequently.mem_of_closed

deleted theorem Filter.HasBasis.clusterPt_iff

deleted theorem Filter.HasBasis.clusterPt_iff_frequently

deleted theorem Filter.HasBasis.lift'_closure

deleted theorem Filter.HasBasis.lift'_closure_eq_self

deleted theorem Filter.HasBasis.lift'_interior

deleted theorem Filter.HasBasis.lift'_interior_eq_self

deleted theorem Filter.HasBasis.mapClusterPt_iff_frequently

deleted theorem Filter.HasBasis.nhds_interior

deleted theorem Filter.Tendsto.lift'_closure

deleted theorem Filter.Tendsto.mapClusterPt

deleted theorem Filter.le_lift'_closure

deleted theorem Filter.lift'_closure_eq_bot

deleted theorem Filter.lift'_interior_le

deleted theorem Finset.closure_biUnion

deleted theorem Finset.interior_iInter

deleted theorem Function.Surjective.denseRange

deleted theorem IsClosed.closure_eq

deleted theorem IsClosed.closure_interior_subset

deleted theorem IsClosed.closure_subset

deleted theorem IsClosed.closure_subset_iff

deleted theorem IsClosed.compl_mem_nhds

deleted theorem IsClosed.frontier_eq

deleted theorem IsClosed.interior_union_left

deleted theorem IsClosed.interior_union_right

deleted theorem IsClosed.mem_iff_closure_subset

deleted theorem IsClosed.mem_of_frequently_of_tendsto

deleted theorem IsClosed.mem_of_tendsto

deleted theorem IsClosed.preimage

deleted theorem IsOpen.closure_inter

deleted theorem IsOpen.eventually_mem

deleted theorem IsOpen.frontier_eq

deleted theorem IsOpen.inter_closure

deleted theorem IsOpen.inter_frontier_eq

deleted theorem IsOpen.interior_eq

deleted theorem IsOpen.mem_nhds

deleted theorem IsOpen.preimage

deleted theorem IsOpen.subset_interior_closure

deleted theorem IsOpen.subset_interior_iff

deleted theorem MapClusterPt.continuousAt_comp

deleted theorem MapClusterPt.frequently

deleted theorem MapClusterPt.mono

deleted theorem MapClusterPt.of_comp

deleted theorem MapClusterPt.tendsto_comp'

deleted theorem MapClusterPt.tendsto_comp

deleted theorem OrderTop.tendsto_atTop_nhds

deleted theorem Set.Finite.closure_biUnion

deleted theorem Set.Finite.closure_sUnion

deleted theorem Set.Finite.interior_biInter

deleted theorem Set.Finite.interior_sInter

deleted theorem Set.MapsTo.closure_left

deleted theorem TopologicalSpace.ext_iff_nhds

deleted theorem accPt_iff_frequently

deleted theorem accPt_iff_nhds

deleted theorem accPt_sup

deleted theorem acc_iff_cluster

deleted theorem acc_principal_iff_cluster

deleted theorem all_mem_nhds

deleted theorem all_mem_nhds_filter

deleted theorem closure_closure

deleted theorem closure_compl

deleted theorem closure_compl_singleton

deleted theorem closure_diff

deleted theorem closure_diff_frontier

deleted theorem closure_diff_interior

deleted theorem closure_empty

deleted theorem closure_empty_iff

deleted theorem closure_eq_cluster_pts

deleted theorem closure_eq_compl_interior_compl

deleted theorem closure_eq_iff_isClosed

deleted theorem closure_eq_interior_union_frontier

deleted theorem closure_eq_self_union_frontier

deleted theorem closure_iUnion_of_finite

deleted theorem closure_iUnion₂_le_nat

deleted theorem closure_iUnion₂_lt_nat

deleted theorem closure_image_closure

deleted theorem closure_inter_open_nonempty_iff

deleted theorem closure_inter_subset_inter_closure

deleted theorem closure_minimal

deleted theorem closure_mono

deleted theorem closure_nonempty_iff

deleted theorem closure_subset_iff_isClosed

deleted theorem closure_subset_preimage_closure_image

deleted theorem closure_union

deleted theorem closure_univ

deleted theorem clusterPt_iff_forall_mem_closure

deleted theorem clusterPt_iff_frequently

deleted theorem clusterPt_iff_lift'_closure'

deleted theorem clusterPt_iff_lift'_closure

deleted theorem clusterPt_iff_nonempty

deleted theorem clusterPt_iff_not_disjoint

deleted theorem clusterPt_lift'_closure_iff

deleted theorem clusterPt_principal

deleted theorem clusterPt_principal_iff

deleted theorem clusterPt_principal_iff_frequently

deleted theorem compl_frontier_eq_union_interior

deleted theorem continuousAt_congr

deleted theorem continuousAt_const

deleted theorem continuousAt_def

deleted theorem continuousAt_id'

deleted theorem continuousAt_id

deleted theorem continuous_congr

deleted theorem continuous_const

deleted theorem continuous_def

deleted theorem continuous_id'

deleted theorem continuous_id

deleted theorem continuous_iff_continuousAt

deleted theorem continuous_iff_isClosed

deleted theorem continuous_of_const

deleted theorem denseRange_id

deleted theorem denseRange_iff_closure_range

deleted theorem denseRange_subtype_val

deleted theorem dense_closure

deleted theorem dense_compl_singleton

deleted theorem dense_compl_singleton_iff_not_open

deleted theorem dense_iff_closure_eq

deleted theorem dense_iff_inter_open

deleted theorem dense_univ

deleted theorem diff_subset_closure_iff

deleted theorem disjoint_frontier_iff_isOpen

deleted theorem disjoint_interior_frontier

deleted theorem eventually_eventuallyEq_nhds

deleted theorem eventually_eventuallyLE_nhds

deleted theorem eventually_eventually_nhds

deleted theorem eventually_mem_nhds_iff

deleted theorem eventually_nhds_iff

deleted theorem exists_open_set_nhds'

deleted theorem exists_open_set_nhds

deleted theorem frequently_frequently_nhds

deleted theorem frequently_nhds_iff

deleted theorem frontier_closure_subset

deleted theorem frontier_compl

deleted theorem frontier_empty

deleted theorem frontier_eq_closure_inter_closure

deleted theorem frontier_eq_inter_compl_interior

deleted theorem frontier_inter_subset

deleted theorem frontier_interior_subset

deleted theorem frontier_subset_closure

deleted theorem frontier_subset_iff_isClosed

deleted theorem frontier_union_subset

deleted theorem frontier_univ

deleted theorem image_closure_subset_closure_image

deleted theorem interior_compl

deleted theorem interior_empty

deleted theorem interior_eq_empty_iff_dense_compl

deleted theorem interior_eq_iff_isOpen

deleted theorem interior_eq_nhds'

deleted theorem interior_eq_nhds

deleted theorem interior_eq_univ

deleted theorem interior_frontier

deleted theorem interior_iInter_of_finite

deleted theorem interior_iInter_subset

deleted theorem interior_iInter₂_le_nat

deleted theorem interior_iInter₂_lt_nat

deleted theorem interior_iInter₂_subset

deleted theorem interior_inter

deleted theorem interior_interior

deleted theorem interior_maximal

deleted theorem interior_mem_nhds

deleted theorem interior_mono

deleted theorem interior_sInter_subset

deleted theorem interior_setOf_eq

deleted theorem interior_singleton

deleted theorem interior_subset

deleted theorem interior_subset_closure

deleted theorem interior_subset_iff

deleted theorem interior_union_isClosed_of_interior_empty

deleted theorem interior_univ

deleted theorem isClosed_closure

deleted theorem isClosed_frontier

deleted theorem isClosed_iff_clusterPt

deleted theorem isClosed_iff_forall_filter

deleted theorem isClosed_iff_frequently

deleted theorem isClosed_iff_nhds

deleted theorem isClosed_of_closure_subset

deleted theorem isClosed_setOf_clusterPt

deleted theorem isOpen_iff_eventually

deleted theorem isOpen_iff_forall_mem_open

deleted theorem isOpen_iff_mem_nhds

deleted theorem isOpen_iff_nhds

deleted theorem isOpen_interior

deleted theorem isOpen_setOf_eventually_nhds

deleted theorem isOpen_singleton_iff_nhds_eq_pure

deleted theorem isOpen_singleton_iff_punctured_nhds

deleted theorem le_nhds_iff

deleted theorem lift'_nhds_interior

deleted theorem mapClusterPt_comp

deleted theorem mapClusterPt_def

deleted theorem mapClusterPt_iff_frequently

deleted theorem map_mem_closure

deleted theorem map_nhds

deleted theorem mem_closure_iff

deleted theorem mem_closure_iff_clusterPt

deleted theorem mem_closure_iff_comap_neBot

deleted theorem mem_closure_iff_frequently

deleted theorem mem_closure_iff_nhds'

deleted theorem mem_closure_iff_nhds

deleted theorem mem_closure_iff_nhdsWithin_neBot

deleted theorem mem_closure_iff_nhds_basis'

deleted theorem mem_closure_iff_nhds_basis

deleted theorem mem_closure_iff_nhds_ne_bot

deleted theorem mem_closure_image

deleted theorem mem_closure_of_frequently_of_tendsto

deleted theorem mem_closure_of_mem_closure_union

deleted theorem mem_closure_of_tendsto

deleted theorem mem_interior

deleted theorem mem_interior_iff_mem_nhds

deleted theorem mem_nhds_iff

deleted theorem mem_of_mem_nhds

deleted theorem monotone_closure

deleted theorem nhdsWithin_mono

deleted theorem nhdsWithin_neBot

deleted theorem nhds_basis_closeds

deleted theorem nhds_basis_opens'

deleted theorem nhds_basis_opens

deleted theorem nhds_bind_nhds

deleted theorem nhds_def'

deleted theorem nhds_le_of_le

deleted theorem not_continuousAt_of_tendsto

deleted theorem not_isOpen_singleton

deleted theorem not_mem_closure_iff_nhdsWithin_eq_bot

deleted theorem not_mem_of_not_mem_closure

deleted theorem preimage_interior_subset_interior_preimage

deleted theorem pure_le_nhds

deleted theorem self_diff_frontier

deleted theorem subset_closure

deleted theorem subset_interior_iff

deleted theorem subset_interior_iff_isOpen

deleted theorem subset_interior_iff_nhds

deleted theorem tendsto_atBot_of_eventually_const

deleted theorem tendsto_atTop_nhds

deleted theorem tendsto_atTop_of_eventually_const

deleted theorem tendsto_const_nhds

deleted theorem tendsto_inf_principal_nhds_iff_of_forall_eq

deleted theorem tendsto_lift'_closure_nhds

deleted theorem tendsto_nhds

deleted theorem tendsto_nhds_of_eventually_eq

deleted theorem tendsto_pure_nhds

Created Mathlib/Topology/Closure.lean

added theorem Dense.exists_mem_open

added theorem Dense.induction

added theorem Dense.interior_compl

added theorem Dense.mono

added theorem Dense.nonempty

added theorem Dense.nonempty_iff

added theorem Disjoint.closure_left

added theorem Disjoint.closure_right

added theorem Disjoint.frontier_left

added theorem Disjoint.frontier_right

added theorem Filter.HasBasis.lift'_closure

added theorem Filter.HasBasis.lift'_closure_eq_self

added theorem Filter.HasBasis.lift'_interior

added theorem Filter.HasBasis.lift'_interior_eq_self

added theorem Filter.le_lift'_closure

added theorem Filter.lift'_closure_eq_bot

added theorem Filter.lift'_interior_le

added theorem Finset.closure_biUnion

added theorem Finset.interior_iInter

added theorem IsClosed.closure_eq

added theorem IsClosed.closure_interior_subset

added theorem IsClosed.closure_subset

added theorem IsClosed.closure_subset_iff

added theorem IsClosed.frontier_eq

added theorem IsClosed.mem_iff_closure_subset

added theorem IsOpen.frontier_eq

added theorem IsOpen.inter_frontier_eq

added theorem IsOpen.interior_eq

added theorem IsOpen.subset_interior_closure

added theorem IsOpen.subset_interior_iff

added theorem Set.Finite.closure_biUnion

added theorem Set.Finite.closure_sUnion

added theorem Set.Finite.interior_biInter

added theorem Set.Finite.interior_sInter

added theorem closure_closure

added theorem closure_compl

added theorem closure_diff_frontier

added theorem closure_diff_interior

added theorem closure_empty

added theorem closure_empty_iff

added theorem closure_eq_compl_interior_compl

added theorem closure_eq_iff_isClosed

added theorem closure_eq_interior_union_frontier

added theorem closure_eq_self_union_frontier

added theorem closure_iUnion_of_finite

added theorem closure_iUnion₂_le_nat

added theorem closure_iUnion₂_lt_nat

added theorem closure_inter_open_nonempty_iff

added theorem closure_inter_subset_inter_closure

added theorem closure_minimal

added theorem closure_mono

added theorem closure_nonempty_iff

added theorem closure_subset_iff_isClosed

added theorem closure_union

added theorem closure_univ

added theorem compl_frontier_eq_union_interior

added theorem dense_closure

added theorem dense_compl_singleton_iff_not_open

added theorem dense_iff_closure_eq

added theorem dense_iff_inter_open

added theorem dense_univ

added theorem diff_subset_closure_iff

added theorem disjoint_frontier_iff_isOpen

added theorem disjoint_interior_frontier

added theorem frontier_closure_subset

added theorem frontier_compl

added theorem frontier_empty

added theorem frontier_eq_closure_inter_closure

added theorem frontier_eq_inter_compl_interior

added theorem frontier_inter_subset

added theorem frontier_interior_subset

added theorem frontier_subset_closure

added theorem frontier_subset_iff_isClosed

added theorem frontier_union_subset

added theorem frontier_univ

added theorem interior_compl

added theorem interior_empty

added theorem interior_eq_empty_iff_dense_compl

added theorem interior_eq_iff_isOpen

added theorem interior_eq_univ

added theorem interior_frontier

added theorem interior_iInter_of_finite

added theorem interior_iInter_subset

added theorem interior_iInter₂_le_nat

added theorem interior_iInter₂_lt_nat

added theorem interior_iInter₂_subset

added theorem interior_inter

added theorem interior_interior

added theorem interior_maximal

added theorem interior_mono

added theorem interior_sInter_subset

added theorem interior_subset

added theorem interior_subset_closure

added theorem interior_subset_iff

added theorem interior_union_isClosed_of_interior_empty

added theorem interior_univ

added theorem isClosed_closure

added theorem isClosed_frontier

added theorem isClosed_of_closure_subset

added theorem isOpen_iff_forall_mem_open

added theorem isOpen_interior

added theorem mem_closure_iff

added theorem mem_interior

added theorem monotone_closure

added theorem not_mem_of_not_mem_closure

added theorem self_diff_frontier

added theorem subset_closure

added theorem subset_interior_iff

added theorem subset_interior_iff_isOpen

Created Mathlib/Topology/ClusterPt.lean

added theorem AccPt.clusterPt

added theorem AccPt.mono

added theorem ClusterPt.frequently

added theorem ClusterPt.mono

added theorem ClusterPt.neBot

added theorem ClusterPt.of_inf_left

added theorem ClusterPt.of_inf_right

added theorem ClusterPt.of_le_nhds'

added theorem ClusterPt.of_le_nhds

added theorem ClusterPt.of_nhds_le

added theorem Filter.EventuallyEq.mapClusterPt_iff

added theorem Filter.HasBasis.clusterPt_iff

added theorem Filter.HasBasis.clusterPt_iff_frequently

added theorem Filter.HasBasis.mapClusterPt_iff_frequently

added theorem Filter.Tendsto.mapClusterPt

added theorem MapClusterPt.continuousAt_comp

added theorem MapClusterPt.frequently

added theorem MapClusterPt.mono

added theorem MapClusterPt.of_comp

added theorem MapClusterPt.tendsto_comp'

added theorem MapClusterPt.tendsto_comp

added theorem accPt_iff_frequently

added theorem accPt_iff_nhds

added theorem accPt_sup

added theorem acc_iff_cluster

added theorem acc_principal_iff_cluster

added theorem closure_compl_singleton

added theorem closure_eq_cluster_pts

added theorem clusterPt_iff_forall_mem_closure

added theorem clusterPt_iff_frequently

added theorem clusterPt_iff_lift'_closure'

added theorem clusterPt_iff_lift'_closure

added theorem clusterPt_iff_nonempty

added theorem clusterPt_iff_not_disjoint

added theorem clusterPt_lift'_closure_iff

added theorem clusterPt_principal

added theorem clusterPt_principal_iff

added theorem clusterPt_principal_iff_frequently

added theorem dense_compl_singleton

added theorem interior_singleton

added theorem isClosed_iff_clusterPt

added theorem isClosed_iff_forall_filter

added theorem isClosed_iff_nhds

added theorem isClosed_setOf_clusterPt

added theorem mapClusterPt_comp

added theorem mapClusterPt_def

added theorem mapClusterPt_iff_frequently

added theorem mem_closure_iff_clusterPt

added theorem mem_closure_iff_comap_neBot

added theorem mem_closure_iff_nhds'

added theorem mem_closure_iff_nhds

added theorem mem_closure_iff_nhdsWithin_neBot

added theorem mem_closure_iff_nhds_basis'

added theorem mem_closure_iff_nhds_basis

added theorem mem_closure_iff_nhds_ne_bot

added theorem mem_closure_of_mem_closure_union

added theorem not_isOpen_singleton

added theorem not_mem_closure_iff_nhdsWithin_eq_bot

Created Mathlib/Topology/Continuous.lean

added theorem ClusterPt.map

added theorem Continuous.closure_preimage_subset

added theorem Continuous.comp'

added theorem Continuous.comp

added theorem Continuous.congr

added theorem Continuous.continuousAt

added theorem Continuous.frontier_preimage_subset

added theorem Continuous.iterate

added theorem Continuous.range_subset_closure_image_dense

added theorem Continuous.tendsto'

added theorem Continuous.tendsto

added theorem ContinuousAt.comp'

added theorem ContinuousAt.comp_of_eq

added theorem ContinuousAt.congr

added theorem ContinuousAt.eventually_mem

added theorem ContinuousAt.iterate

added theorem ContinuousAt.preimage_mem_nhds

added theorem ContinuousAt.tendsto

added theorem Dense.denseRange_val

added theorem DenseRange.closure_range

added theorem DenseRange.comp

added theorem DenseRange.dense_image

added theorem DenseRange.dense_of_mapsTo

added theorem DenseRange.mem_nhds

added theorem DenseRange.nonempty

added theorem DenseRange.subset_closure_image_preimage_of_isOpen

added theorem Equiv.continuous_symm_iff

added theorem Equiv.isOpenMap_symm_iff

added theorem Filter.EventuallyEq.continuousAt

added theorem Filter.Tendsto.lift'_closure

added theorem Function.Surjective.denseRange

added theorem IsClosed.preimage

added theorem IsOpen.preimage

added theorem Set.MapsTo.closure_left

added theorem closure_image_closure

added theorem closure_subset_preimage_closure_image

added theorem continuousAt_congr

added theorem continuousAt_const

added theorem continuousAt_def

added theorem continuousAt_id'

added theorem continuousAt_id

added theorem continuous_congr

added theorem continuous_const

added theorem continuous_def

added theorem continuous_id'

added theorem continuous_id

added theorem continuous_iff_continuousAt

added theorem continuous_iff_isClosed

added theorem continuous_of_const

added theorem denseRange_id

added theorem denseRange_iff_closure_range

added theorem denseRange_subtype_val

added theorem image_closure_subset_closure_image

added theorem map_mem_closure

added theorem mem_closure_image

added theorem not_continuousAt_of_tendsto

added theorem preimage_interior_subset_interior_preimage

added theorem tendsto_lift'_closure_nhds

Modified Mathlib/Topology/Defs/Induced.lean

Modified Mathlib/Topology/GDelta/Basic.lean

Modified Mathlib/Topology/MetricSpace/Thickening.lean

Modified Mathlib/Topology/Metrizable/CompletelyMetrizable.lean

Created Mathlib/Topology/Neighborhoods.lean

added theorem Dense.inter_nhds_nonempty

added theorem Dense.inter_of_isOpen_left

added theorem Dense.inter_of_isOpen_right

added theorem Dense.open_subset_closure_inter

added theorem Filter.Eventually.eventually_nhds

added theorem Filter.Eventually.self_of_nhds

added theorem Filter.EventuallyEq.eq_of_nhds

added theorem Filter.EventuallyEq.eventuallyEq_nhds

added theorem Filter.EventuallyEq.tendsto

added theorem Filter.EventuallyLE.eventuallyLE_nhds

added theorem Filter.Frequently.mem_of_closed

added theorem Filter.HasBasis.nhds_interior

added theorem IsClosed.compl_mem_nhds

added theorem IsClosed.interior_union_left

added theorem IsClosed.interior_union_right

added theorem IsClosed.mem_of_frequently_of_tendsto

added theorem IsClosed.mem_of_tendsto

added theorem IsOpen.closure_inter

added theorem IsOpen.eventually_mem

added theorem IsOpen.inter_closure

added theorem IsOpen.mem_nhds

added theorem OrderTop.tendsto_atTop_nhds

added theorem TopologicalSpace.ext_iff_nhds

added theorem all_mem_nhds

added theorem all_mem_nhds_filter

added theorem closure_diff

added theorem eventually_eventuallyEq_nhds

added theorem eventually_eventuallyLE_nhds

added theorem eventually_eventually_nhds

added theorem eventually_mem_nhds_iff

added theorem eventually_nhds_iff

added theorem exists_open_set_nhds'

added theorem exists_open_set_nhds

added theorem frequently_frequently_nhds

added theorem frequently_nhds_iff

added theorem interior_eq_nhds'

added theorem interior_eq_nhds

added theorem interior_mem_nhds

added theorem interior_setOf_eq

added theorem isClosed_iff_frequently

added theorem isOpen_iff_eventually

added theorem isOpen_iff_mem_nhds

added theorem isOpen_iff_nhds

added theorem isOpen_setOf_eventually_nhds

added theorem isOpen_singleton_iff_nhds_eq_pure

added theorem isOpen_singleton_iff_punctured_nhds

added theorem le_nhds_iff

added theorem lift'_nhds_interior

added theorem map_nhds

added theorem mem_closure_iff_frequently

added theorem mem_closure_of_frequently_of_tendsto

added theorem mem_closure_of_tendsto

added theorem mem_interior_iff_mem_nhds

added theorem mem_nhds_iff

added theorem mem_of_mem_nhds

added theorem nhdsWithin_mono

added theorem nhdsWithin_neBot

added theorem nhds_basis_closeds

added theorem nhds_basis_opens'

added theorem nhds_basis_opens

added theorem nhds_bind_nhds

added theorem nhds_def'

added theorem nhds_le_of_le

added theorem pure_le_nhds

added theorem subset_interior_iff_nhds

added theorem tendsto_atBot_of_eventually_const

added theorem tendsto_atTop_nhds

added theorem tendsto_atTop_of_eventually_const

added theorem tendsto_const_nhds

added theorem tendsto_inf_principal_nhds_iff_of_forall_eq

added theorem tendsto_nhds

added theorem tendsto_nhds_of_eventually_eq

added theorem tendsto_pure_nhds

Modified Mathlib/Topology/NhdsSet.lean

Modified Mathlib/Topology/Order.lean

Modified Mathlib/Topology/Order/Hom/Basic.lean

Modified Mathlib/Topology/Partial.lean

Modified Mathlib/Topology/Separation/SeparatedNhds.lean

Modified Mathlib/Topology/Ultrafilter.lean