Commit 2024-01-26 03:44 20c7b4b8

View on Github →

chore(Topology/Basic): re-use variables; rename a : X to x : X (#9993)

Estimated changes

modified theorem AccPt.mono
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 theorem Continuous.comp'
modified theorem Continuous.comp
modified theorem Continuous.congr
modified theorem Continuous.continuousAt
modified theorem Continuous.tendsto'
modified theorem Continuous.tendsto
modified theorem ContinuousAt.comp_of_eq
modified theorem ContinuousAt.congr
modified theorem ContinuousAt.iterate
modified theorem ContinuousAt.tendsto
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 DenseRange.dense_image
modified theorem DenseRange.dense_of_mapsTo
modified theorem DenseRange.mem_nhds
modified def DenseRange.some
modified theorem Disjoint.closure_left
modified theorem Disjoint.closure_right
modified theorem Filter.EventuallyEq.tendsto
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.mem_of_tendsto
modified theorem IsClosed.preimage
modified theorem IsClosed.sdiff
modified theorem IsOpen.and
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 theorem Set.MapsTo.closure_left
modified theorem Ultrafilter.clusterPt_iff
modified theorem closure_closure
modified theorem closure_compl
modified theorem closure_diff
modified theorem closure_eq_cluster_pts
modified theorem closure_eq_iff_isClosed
modified theorem closure_image_closure
modified theorem closure_minimal
modified theorem closure_mono
modified theorem closure_nonempty_iff
modified theorem closure_subset_iff_isClosed
modified theorem closure_union
modified theorem clusterPt_iff
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 continuousAt_congr
modified theorem continuousAt_const
modified theorem continuousAt_def
modified theorem continuousAt_id
modified theorem continuous_congr
modified theorem continuous_const
modified theorem continuous_def
modified theorem continuous_iff_continuousAt
modified theorem continuous_iff_isClosed
modified theorem continuous_iff_ultrafilter
modified theorem continuous_of_const
modified theorem dense_closure
modified theorem dense_iff_closure_eq
modified theorem dense_iff_inter_open
modified theorem diff_subset_closure_iff
modified theorem eventuallyEq_zero_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 theorem frontier_closure_subset
modified theorem frontier_interior_subset
modified theorem frontier_subset_closure
modified theorem interior_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_inter
modified theorem interior_interior
modified theorem interior_maximal
modified theorem interior_mem_nhds
modified theorem interior_mono
modified theorem interior_subset
modified theorem interior_subset_closure
modified theorem isClosed_closure
modified theorem isClosed_const
modified theorem isClosed_frontier
modified theorem isClosed_iff_clusterPt
modified theorem isClosed_iff_forall_filter
modified theorem isClosed_iff_frequently
modified theorem isClosed_iff_nhds
modified theorem isClosed_of_closure_subset
modified theorem isOpen_compl_iff
modified theorem isOpen_const
modified theorem isOpen_fold
modified theorem isOpen_iff_eventually
modified theorem isOpen_iff_mem_nhds
modified theorem isOpen_iff_nhds
modified theorem isOpen_iff_ultrafilter
modified theorem isOpen_interior
modified theorem isOpen_mk
modified theorem le_nhds_iff
modified theorem le_nhds_lim
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_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_tendsto
modified theorem mem_interior
modified theorem mem_interior_iff_mem_nhds
modified theorem mem_nhds_iff
modified theorem mem_of_mem_nhds
modified def nhdsWithin
modified theorem nhds_basis_closeds
modified theorem nhds_basis_opens'
modified theorem nhds_basis_opens
modified theorem nhds_bind_nhds
modified theorem nhds_def'
modified theorem nhds_le_of_le
modified theorem not_mem_of_not_mem_closure
modified theorem subset_closure
modified theorem subset_interior_iff
modified theorem subset_interior_iff_isOpen
modified theorem subset_interior_iff_nhds
modified theorem tendsto_atTop_nhds
modified theorem tendsto_const_nhds
modified theorem tendsto_nhds
modified theorem tendsto_nhds_limUnder