Commit 2023-01-26 08:19 e8f582b4

View on Github →

feat: port Topology.Basic (#1826)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Basic.lean

added theorem AccPt.mono

added def AccPt

added theorem ClusterPt.map

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 def ClusterPt

added theorem Continuous.closure_preimage_subset

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 structure Continuous

added theorem ContinuousAt.congr

added theorem ContinuousAt.iterate

added theorem ContinuousAt.preimage_mem_nhds

added theorem ContinuousAt.tendsto

added def ContinuousAt

added theorem Dense.denseRange_val

added theorem Dense.exists_mem_open

added theorem Dense.inter_nhds_nonempty

added theorem Dense.inter_of_open_left

added theorem Dense.inter_of_open_right

added theorem Dense.interior_compl

added theorem Dense.mono

added theorem Dense.nonempty

added theorem Dense.nonempty_iff

added theorem Dense.open_subset_closure_inter

added def Dense

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 def DenseRange.some

added theorem DenseRange.subset_closure_image_preimage_of_isOpen

added def DenseRange

added theorem Disjoint.closure_left

added theorem Disjoint.closure_right

added theorem Disjoint.frontier_left

added theorem Disjoint.frontier_right

added theorem Filter.Eventually.eventually_nhds

added theorem Filter.Eventually.self_of_nhds

added theorem Filter.EventuallyEq.continuousAt

added theorem Filter.EventuallyEq.eq_of_nhds

added theorem Filter.EventuallyEq.eventuallyEq_nhds

added theorem Filter.EventuallyLe.eventuallyLe_nhds

added theorem Filter.Frequently.mem_of_closed

added theorem Filter.HasBasis.clusterPt_iff

added theorem Filter.HasBasis.lift'_closure

added theorem Filter.HasBasis.lift'_closure_eq_self

added theorem Filter.le_lift'_closure

added theorem Filter.lift'_closure_eq_bot

added theorem Finset.closure_bunionᵢ

added theorem Finset.interior_interᵢ

added theorem Function.Surjective.denseRange

added theorem IsClosed.closure_eq

added theorem IsClosed.closure_subset

added theorem IsClosed.closure_subset_iff

added theorem IsClosed.compl_mem_nhds

added theorem IsClosed.frontier_eq

added theorem IsClosed.frontier_subset

added theorem IsClosed.inter

added theorem IsClosed.interior_union_left

added theorem IsClosed.interior_union_right

added theorem IsClosed.mem_iff_closure_subset

added theorem IsClosed.mem_of_frequently_of_tendsto

added theorem IsClosed.mem_of_tendsto

added theorem IsClosed.not

added theorem IsClosed.preimage

added theorem IsClosed.sdiff

added theorem IsClosed.union

added theorem IsOpen.and

added theorem IsOpen.closure_inter

added theorem IsOpen.eventually_mem

added theorem IsOpen.frontier_eq

added theorem IsOpen.inter

added theorem IsOpen.inter_closure

added theorem IsOpen.inter_frontier_eq

added theorem IsOpen.interior_eq

added theorem IsOpen.mem_nhds

added theorem IsOpen.preimage

added theorem IsOpen.sdiff

added theorem IsOpen.subset_interior_iff

added theorem IsOpen.union

added def IsOpen

added def MapClusterPt

added theorem OrderTop.tendsto_atTop_nhds

added theorem Set.MapsTo.closure_left

added def TopologicalSpace.ofClosed

added structure TopologicalSpace

added theorem Ultrafilter.clusterPt_iff

added theorem accPt_iff_frequently

added theorem accPt_iff_nhds

added theorem acc_iff_cluster

added theorem acc_principal_iff_cluster

added theorem all_mem_nhds

added theorem all_mem_nhds_filter

added def closure

added theorem closure_closure

added theorem closure_compl

added theorem closure_compl_singleton

added theorem closure_diff

added theorem closure_diff_frontier

added theorem closure_diff_interior

added theorem closure_empty

added theorem closure_empty_iff

added theorem closure_eq_cluster_pts

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_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_subset_preimage_closure_image

added theorem closure_union

added theorem closure_unionᵢ

added theorem closure_univ

added theorem clusterPt_iff

added theorem clusterPt_principal_iff

added theorem clusterPt_principal_iff_frequently

added theorem compl_frontier_eq_union_interior

added theorem continuousAt_congr

added theorem continuousAt_const

added theorem continuousAt_def

added theorem continuousAt_id

added theorem continuousAt_iff_ultrafilter

added theorem continuous_const

added theorem continuous_def

added theorem continuous_id

added theorem continuous_iff_continuousAt

added theorem continuous_iff_isClosed

added theorem continuous_iff_ultrafilter

added theorem continuous_of_const

added theorem denseRange_id

added theorem denseRange_iff_closure_range

added theorem dense_closure

added theorem dense_compl_singleton

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 eventuallyEq_zero_nhds

added theorem eventually_eventuallyEq_nhds

added theorem eventually_eventuallyLe_nhds

added theorem eventually_eventually_nhds

added theorem eventually_mem_nhds

added theorem eventually_nhds_iff

added theorem exists_open_set_nhds'

added theorem exists_open_set_nhds

added theorem frequently_frequently_nhds

added def 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_union_subset

added theorem frontier_univ

added theorem image_closure_subset_closure_image

added def interior

added theorem interior_Inter₂_subset

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_nhds'

added theorem interior_eq_nhds

added theorem interior_eq_univ

added theorem interior_frontier

added theorem interior_inter

added theorem interior_interior

added theorem interior_interᵢ

added theorem interior_interᵢ_subset

added theorem interior_interₛ_subset

added theorem interior_maximal

added theorem interior_mem_nhds

added theorem interior_mono

added theorem interior_setOf_eq

added theorem interior_singleton

added theorem interior_subset

added theorem interior_subset_closure

added theorem interior_union_isClosed_of_interior_empty

added theorem interior_univ

added theorem isClosed_binterᵢ

added theorem isClosed_bunionᵢ

added theorem isClosed_closure

added theorem isClosed_compl_iff

added theorem isClosed_const

added theorem isClosed_empty

added theorem isClosed_frontier

added theorem isClosed_iff_clusterPt

added theorem isClosed_iff_frequently

added theorem isClosed_iff_nhds

added theorem isClosed_imp

added theorem isClosed_interᵢ

added theorem isClosed_interₛ

added theorem isClosed_of_closure_subset

added theorem isClosed_setOf_clusterPt

added theorem isClosed_unionᵢ

added theorem isClosed_unionᵢ_prop

added theorem isClosed_univ

added theorem isOpen_binterᵢ

added theorem isOpen_binterᵢ_finset

added theorem isOpen_bunionᵢ

added theorem isOpen_compl_iff

added theorem isOpen_const

added theorem isOpen_empty

added theorem isOpen_fold

added theorem isOpen_iff_eventually

added theorem isOpen_iff_forall_mem_open

added theorem isOpen_iff_mem_nhds

added theorem isOpen_iff_nhds

added theorem isOpen_iff_ultrafilter

added theorem isOpen_interior

added theorem isOpen_interᵢ

added theorem isOpen_interᵢ_prop

added theorem isOpen_interₛ

added theorem isOpen_setOf_eventually_nhds

added theorem isOpen_singleton_iff_nhds_eq_pure

added theorem isOpen_singleton_iff_punctured_nhds

added theorem isOpen_unionᵢ

added theorem isOpen_unionₛ

added theorem isOpen_univ

added theorem le_nhds_iff

added theorem le_nhds_lim

added theorem mapClusterPt_iff

added theorem mapClusterPt_of_comp

added theorem map_mem_closure

added theorem map_nhds

added theorem mem_closure_iff

added theorem mem_closure_iff_clusterPt

added theorem mem_closure_iff_comap_neBot

added theorem mem_closure_iff_frequently

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_neBot

added theorem mem_closure_iff_ultrafilter

added theorem mem_closure_image

added theorem mem_closure_of_frequently_of_tendsto

added theorem mem_closure_of_mem_closure_union

added theorem mem_closure_of_tendsto

added theorem mem_interior

added theorem mem_interior_iff_mem_nhds

added theorem mem_nhds_iff

added theorem mem_of_mem_nhds

added theorem monotone_closure

added def nhdsWithin

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 not_isOpen_singleton

added theorem not_mem_of_not_mem_closure

added theorem preimage_interior_subset_interior_preimage

added theorem pure_le_nhds

added theorem self_diff_frontier

added theorem subset_closure

added theorem subset_interior_iff

added theorem subset_interior_iff_isOpen

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_limUnder

added theorem tendsto_pure_nhds

added theorem topologicalSpace_eq

added theorem topologicalSpace_eq_iff