Commit 2024-01-24 10:41 6694f75a

View on Github →

chore(Topology/Basic): rename variables (#9956) Use X, Y, Z for topological spaces.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

Modified Mathlib/Topology/Basic.lean

modified theorem AccPt.mono

modified def AccPt

modified theorem ClusterPt.map

modified theorem ClusterPt.mono

modified theorem ClusterPt.neBot

modified theorem ClusterPt.of_inf_left

modified theorem ClusterPt.of_inf_right

modified theorem ClusterPt.of_le_nhds'

modified theorem ClusterPt.of_le_nhds

modified theorem ClusterPt.of_nhds_le

modified def ClusterPt

modified theorem Continuous.closure_preimage_subset

modified theorem Continuous.comp'

modified theorem Continuous.comp

modified theorem Continuous.congr

modified theorem Continuous.continuousAt

modified theorem Continuous.frontier_preimage_subset

modified theorem Continuous.iterate

modified theorem Continuous.range_subset_closure_image_dense

modified theorem Continuous.tendsto'

modified theorem Continuous.tendsto

modified structure Continuous

modified theorem ContinuousAt.comp_of_eq

modified theorem ContinuousAt.congr

modified theorem ContinuousAt.iterate

modified theorem ContinuousAt.preimage_mem_nhds

modified theorem ContinuousAt.tendsto

modified def ContinuousAt

modified theorem Dense.denseRange_val

modified theorem Dense.exists_mem_open

modified theorem Dense.inter_nhds_nonempty

modified theorem Dense.inter_of_isOpen_left

modified theorem Dense.inter_of_isOpen_right

modified theorem Dense.interior_compl

modified theorem Dense.mono

modified theorem Dense.nonempty

modified theorem Dense.nonempty_iff

modified theorem Dense.open_subset_closure_inter

modified def Dense

modified theorem DenseRange.comp

modified theorem DenseRange.dense_image

modified theorem DenseRange.dense_of_mapsTo

modified theorem DenseRange.mem_nhds

modified theorem DenseRange.nonempty

modified def DenseRange.some

modified theorem DenseRange.subset_closure_image_preimage_of_isOpen

modified theorem Disjoint.closure_left

modified theorem Disjoint.closure_right

modified theorem Filter.Eventually.eventually_nhds

modified theorem Filter.Eventually.self_of_nhds

modified theorem Filter.EventuallyEq.continuousAt

modified theorem Filter.EventuallyEq.eq_of_nhds

modified theorem Filter.EventuallyEq.eventuallyEq_nhds

modified theorem Filter.EventuallyEq.tendsto

modified theorem Filter.EventuallyLE.eventuallyLE_nhds

modified theorem Filter.Frequently.mem_of_closed

modified theorem Filter.HasBasis.clusterPt_iff

modified theorem Filter.HasBasis.lift'_closure

modified theorem Filter.HasBasis.lift'_closure_eq_self

modified theorem Filter.le_lift'_closure

modified theorem Filter.lift'_closure_eq_bot

modified theorem Finset.closure_biUnion

modified theorem Finset.interior_iInter

modified theorem IsClosed.closure_eq

modified theorem IsClosed.closure_subset

modified theorem IsClosed.closure_subset_iff

modified theorem IsClosed.compl_mem_nhds

modified theorem IsClosed.frontier_eq

modified theorem IsClosed.interior_union_left

modified theorem IsClosed.interior_union_right

modified theorem IsClosed.mem_iff_closure_subset

modified theorem IsClosed.mem_of_frequently_of_tendsto

modified theorem IsClosed.mem_of_tendsto

modified theorem IsClosed.preimage

modified theorem IsClosed.sdiff

modified theorem IsOpen.closure_inter

modified theorem IsOpen.eventually_mem

modified theorem IsOpen.frontier_eq

modified theorem IsOpen.inter_closure

modified theorem IsOpen.inter_frontier_eq

modified theorem IsOpen.interior_eq

modified theorem IsOpen.mem_nhds

modified theorem IsOpen.preimage

modified theorem IsOpen.sdiff

modified theorem IsOpen.subset_interior_iff

modified def IsOpen

modified def MapClusterPt

modified theorem OrderTop.tendsto_atTop_nhds

modified theorem Set.Finite.closure_biUnion

modified theorem Set.Finite.closure_sUnion

modified theorem Set.Finite.interior_biInter

modified theorem Set.Finite.interior_sInter

modified theorem Set.Finite.isClosed_biUnion

modified theorem Set.Finite.isOpen_biInter

modified theorem Set.Finite.isOpen_sInter

modified theorem Set.MapsTo.closure_left

modified def TopologicalSpace.ofClosed

modified theorem Ultrafilter.clusterPt_iff

modified theorem accPt_iff_frequently

modified theorem accPt_iff_nhds

modified theorem acc_iff_cluster

modified theorem acc_principal_iff_cluster

modified theorem all_mem_nhds

modified theorem all_mem_nhds_filter

modified def closure

modified theorem closure_closure

modified theorem closure_compl

modified theorem closure_compl_singleton

modified theorem closure_diff

modified theorem closure_diff_frontier

modified theorem closure_diff_interior

modified theorem closure_empty

modified theorem closure_empty_iff

modified theorem closure_eq_cluster_pts

modified theorem closure_eq_compl_interior_compl

modified theorem closure_eq_iff_isClosed

modified theorem closure_eq_interior_union_frontier

modified theorem closure_eq_self_union_frontier

modified theorem closure_iUnion_of_finite

modified theorem closure_image_closure

modified theorem closure_inter_open_nonempty_iff

modified theorem closure_inter_subset_inter_closure

modified theorem closure_minimal

modified theorem closure_mono

modified theorem closure_nonempty_iff

modified theorem closure_subset_iff_isClosed

modified theorem closure_subset_preimage_closure_image

modified theorem closure_union

modified theorem closure_univ

modified theorem clusterPt_iff

modified theorem clusterPt_iff_forall_mem_closure

modified theorem clusterPt_iff_lift'_closure'

modified theorem clusterPt_iff_lift'_closure

modified theorem clusterPt_iff_not_disjoint

modified theorem clusterPt_lift'_closure_iff

modified theorem clusterPt_principal_iff

modified theorem clusterPt_principal_iff_frequently

modified theorem compl_frontier_eq_union_interior

modified theorem continuousAt_congr

modified theorem continuousAt_const

modified theorem continuousAt_def

modified theorem continuousAt_id

modified theorem continuousAt_iff_ultrafilter

modified theorem continuous_congr

modified theorem continuous_const

modified theorem continuous_def

modified theorem continuous_id'

modified theorem continuous_id

modified theorem continuous_iff_continuousAt

modified theorem continuous_iff_isClosed

modified theorem continuous_iff_ultrafilter

modified theorem continuous_of_const

modified theorem denseRange_id

modified theorem dense_closure

modified theorem dense_compl_singleton

modified theorem dense_compl_singleton_iff_not_open

modified theorem dense_iff_closure_eq

modified theorem dense_iff_inter_open

modified theorem dense_univ

modified theorem diff_subset_closure_iff

modified theorem eventuallyEq_zero_nhds

modified theorem eventually_eventuallyEq_nhds

modified theorem eventually_eventuallyLE_nhds

modified theorem eventually_eventually_nhds

modified theorem eventually_mem_nhds

modified theorem eventually_nhds_iff

modified theorem exists_open_set_nhds'

modified theorem exists_open_set_nhds

modified theorem frequently_frequently_nhds

modified def frontier

modified theorem frontier_closure_subset

modified theorem frontier_compl

modified theorem frontier_empty

modified theorem frontier_eq_closure_inter_closure

modified theorem frontier_eq_inter_compl_interior

modified theorem frontier_inter_subset

modified theorem frontier_interior_subset

modified theorem frontier_subset_closure

modified theorem frontier_union_subset

modified theorem frontier_univ

modified theorem image_closure_subset_closure_image

modified def interior

modified theorem interior_compl

modified theorem interior_empty

modified theorem interior_eq_empty_iff_dense_compl

modified theorem interior_eq_iff_isOpen

modified theorem interior_eq_nhds'

modified theorem interior_eq_nhds

modified theorem interior_eq_univ

modified theorem interior_frontier

modified theorem interior_iInter_of_finite

modified theorem interior_iInter_subset

modified theorem interior_iInter₂_subset

modified theorem interior_inter

modified theorem interior_interior

modified theorem interior_maximal

modified theorem interior_mem_nhds

modified theorem interior_mono

modified theorem interior_sInter_subset

modified theorem interior_setOf_eq

modified theorem interior_singleton

modified theorem interior_subset

modified theorem interior_subset_closure

modified theorem interior_union_isClosed_of_interior_empty

modified theorem interior_univ

modified theorem isClosed_biInter

modified theorem isClosed_biUnion_finset

modified theorem isClosed_closure

modified theorem isClosed_compl_iff

modified theorem isClosed_const

modified theorem isClosed_empty

modified theorem isClosed_frontier

modified theorem isClosed_iInter

modified theorem isClosed_iUnion_of_finite

modified theorem isClosed_iff_clusterPt

modified theorem isClosed_iff_forall_filter

modified theorem isClosed_iff_frequently

modified theorem isClosed_iff_nhds

modified theorem isClosed_imp

modified theorem isClosed_of_closure_subset

modified theorem isClosed_sInter

modified theorem isClosed_setOf_clusterPt

modified theorem isClosed_univ

modified theorem isOpen_biInter_finset

modified theorem isOpen_biUnion

modified theorem isOpen_compl_iff

modified theorem isOpen_const

modified theorem isOpen_empty

modified theorem isOpen_fold

modified theorem isOpen_iInter_of_finite

modified theorem isOpen_iUnion

modified theorem isOpen_iff_eventually

modified theorem isOpen_iff_mem_nhds

modified theorem isOpen_iff_nhds

modified theorem isOpen_iff_of_cover

modified theorem isOpen_iff_ultrafilter

modified theorem isOpen_interior

modified theorem isOpen_mk

modified theorem isOpen_sUnion

modified theorem isOpen_setOf_eventually_nhds

modified theorem isOpen_singleton_iff_nhds_eq_pure

modified theorem isOpen_singleton_iff_punctured_nhds

modified theorem isOpen_univ

modified theorem le_nhds_iff

modified theorem le_nhds_lim

modified theorem mapClusterPt_iff

modified theorem mapClusterPt_of_comp

modified theorem map_mem_closure

modified theorem map_nhds

modified theorem mem_closure_iff

modified theorem mem_closure_iff_clusterPt

modified theorem mem_closure_iff_comap_neBot

modified theorem mem_closure_iff_frequently

modified theorem mem_closure_iff_nhds'

modified theorem mem_closure_iff_nhds

modified theorem mem_closure_iff_nhdsWithin_neBot

modified theorem mem_closure_iff_nhds_basis'

modified theorem mem_closure_iff_nhds_basis

modified theorem mem_closure_iff_nhds_neBot

modified theorem mem_closure_iff_ultrafilter

modified theorem mem_closure_image

modified theorem mem_closure_of_frequently_of_tendsto

modified theorem mem_closure_of_mem_closure_union

modified theorem mem_closure_of_tendsto

modified theorem mem_interior

modified theorem mem_interior_iff_mem_nhds

modified theorem mem_nhds_iff

modified theorem mem_of_mem_nhds

modified theorem monotone_closure

modified def nhdsWithin

modified theorem nhds_basis_closeds

modified theorem nhds_basis_opens'

modified theorem nhds_basis_opens

modified theorem nhds_def'

modified theorem nhds_le_of_le

modified theorem not_isOpen_singleton

modified theorem not_mem_closure_iff_nhdsWithin_eq_bot

modified theorem not_mem_of_not_mem_closure

modified theorem preimage_interior_subset_interior_preimage

modified theorem pure_le_nhds

modified theorem self_diff_frontier

modified theorem subset_closure

modified theorem subset_interior_iff

modified theorem subset_interior_iff_isOpen

modified theorem subset_interior_iff_nhds

modified theorem tendsto_atBot_of_eventually_const

modified theorem tendsto_atTop_nhds

modified theorem tendsto_atTop_of_eventually_const

modified theorem tendsto_const_nhds

modified theorem tendsto_inf_principal_nhds_iff_of_forall_eq

modified theorem tendsto_nhds

modified theorem tendsto_nhds_limUnder

modified theorem tendsto_nhds_of_eventually_eq

modified theorem tendsto_pure_nhds

Modified Mathlib/Topology/MetricSpace/Polish.lean