Mathlib Changelog
v4
Changelog
About
Github
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
Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
Modified
Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection.lean
Modified
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
Modified
Mathlib/Topology/Algebra/Algebra.lean
Modified
Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
Modified
Mathlib/Topology/Bases.lean
Modified
Mathlib/Topology/Basic.lean
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.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.range_subset_closure_image_dense
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.preimage_mem_nhds
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
Dense.open_subset_closure_inter
modified
theorem
DenseRange.dense_image
modified
theorem
DenseRange.dense_of_mapsTo
modified
theorem
DenseRange.mem_nhds
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
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.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_compl_interior_compl
modified
theorem
closure_eq_iff_isClosed
modified
theorem
closure_image_closure
modified
theorem
closure_inter_open_nonempty_iff
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
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_iff_continuousAt
modified
theorem
continuous_iff_isClosed
modified
theorem
continuous_iff_ultrafilter
modified
theorem
continuous_of_const
modified
theorem
dense_closure
modified
theorem
dense_compl_singleton_iff_not_open
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_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
theorem
frontier_closure_subset
modified
theorem
frontier_eq_closure_inter_closure
modified
theorem
frontier_eq_inter_compl_interior
modified
theorem
frontier_interior_subset
modified
theorem
frontier_subset_closure
modified
theorem
image_closure_subset_closure_image
modified
theorem
interior_compl
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_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
interior_union_isClosed_of_interior_empty
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
isOpen_singleton_iff_nhds_eq_pure
modified
theorem
isOpen_singleton_iff_punctured_nhds
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_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
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_closure_iff_nhdsWithin_eq_bot
modified
theorem
not_mem_of_not_mem_closure
modified
theorem
preimage_interior_subset_interior_preimage
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
Mathlib/Topology/Category/Profinite/Nobeling.lean
Modified
Mathlib/Topology/MetricSpace/HausdorffDistance.lean
Modified
Mathlib/Topology/Order.lean
Modified
Mathlib/Topology/UniformSpace/Basic.lean
Modified
Mathlib/Topology/UniformSpace/CompactConvergence.lean