Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-11-12 11:23
2cbeed95
View on Github →
style(*): use notation
𝓝
for
nhds
(
#1582
)
chore(*): notation for nhds
Convert new uses of nhds
Estimated changes
Modified
docs/contribute/style.md
Modified
docs/theories/topology.md
Modified
src/analysis/asymptotics.lean
Modified
src/analysis/calculus/fderiv.lean
modified
theorem
differentiable_within_at_inter
modified
theorem
fderiv_congr_of_mem_nhds
modified
theorem
fderiv_within_inter
modified
theorem
has_fderiv_at.has_fderiv_at_filter
modified
theorem
has_fderiv_within_at_inter
Modified
src/analysis/calculus/tangent_cone.lean
modified
theorem
tangent_cone_inter_nhds
modified
theorem
unique_diff_within_at.inter
modified
theorem
unique_diff_within_at_inter
Modified
src/analysis/calculus/times_cont_diff.lean
modified
theorem
iterated_fderiv_within_inter
Modified
src/analysis/complex/exponential.lean
modified
theorem
complex.tendsto_exp_zero_one
modified
theorem
real.tendsto_log_one_zero
Modified
src/analysis/normed_space/banach.lean
Modified
src/analysis/normed_space/basic.lean
Modified
src/analysis/normed_space/real_inner_product.lean
Modified
src/analysis/specific_limits.lean
modified
theorem
tendsto_inverse_at_top_nhds_0
modified
theorem
tendsto_inverse_at_top_nhds_0_nat
modified
theorem
tendsto_one_div_at_top_nhds_0_nat
Modified
src/data/analysis/topology.lean
Modified
src/data/padics/hensel.lean
Modified
src/data/real/hyperreal.lean
modified
theorem
hyperreal.gt_of_tendsto_zero_of_neg
modified
theorem
hyperreal.is_st_of_tendsto
modified
theorem
hyperreal.lt_of_tendsto_zero_of_pos
modified
theorem
hyperreal.neg_lt_of_tendsto_zero_of_pos
Modified
src/measure_theory/decomposition.lean
Modified
src/measure_theory/integration.lean
Modified
src/measure_theory/measure_space.lean
Modified
src/measure_theory/simple_func_dense.lean
Modified
src/order/filter/pointwise.lean
Modified
src/topology/algebra/group.lean
modified
theorem
add_group_with_zero_nhd.nhds_eq
modified
theorem
add_group_with_zero_nhd.nhds_zero_eq_Z
modified
theorem
exists_nhds_split4
modified
theorem
exists_nhds_split
modified
theorem
exists_nhds_split_inv
modified
theorem
nhds_is_mul_hom
modified
theorem
nhds_one_symm
modified
theorem
nhds_pointwise_mul
modified
theorem
nhds_translation
Modified
src/topology/algebra/infinite_sum.lean
modified
def
has_sum
Modified
src/topology/algebra/monoid.lean
modified
theorem
tendsto_mul'
Modified
src/topology/algebra/open_subgroup.lean
modified
theorem
open_subgroup.mem_nhds_one
Modified
src/topology/algebra/ordered.lean
modified
theorem
Liminf_eq_of_le_nhds
modified
theorem
Liminf_nhds
modified
theorem
Limsup_eq_of_le_nhds
modified
theorem
Limsup_nhds
modified
theorem
ge_mem_nhds
modified
theorem
gt_mem_nhds
modified
theorem
is_bounded_ge_nhds
modified
theorem
is_bounded_le_nhds
modified
theorem
is_cobounded_ge_nhds
modified
theorem
is_cobounded_le_nhds
modified
theorem
le_mem_nhds
modified
theorem
lt_mem_nhds
modified
theorem
mem_nhds_orderable_dest
modified
theorem
tendsto_max
modified
theorem
tendsto_min
Modified
src/topology/algebra/uniform_group.lean
modified
theorem
is_Z_bilin.tendsto_zero_left
modified
theorem
is_Z_bilin.tendsto_zero_right
modified
theorem
uniformity_eq_comap_nhds_zero'
modified
theorem
uniformity_eq_comap_nhds_zero
Modified
src/topology/bases.lean
Modified
src/topology/basic.lean
modified
theorem
closure_eq_nhds
modified
def
continuous_at
modified
theorem
interior_eq_nhds
modified
theorem
is_closed_iff_nhds
modified
theorem
is_open_iff_mem_nhds
modified
theorem
is_open_iff_nhds
modified
theorem
le_nhds_iff
modified
theorem
lim_spec
modified
theorem
mem_closure_iff_nhds
modified
theorem
mem_of_nhds
modified
theorem
nhds_def
modified
theorem
nhds_le_of_le
modified
theorem
nhds_neq_bot
modified
theorem
nhds_sets
modified
theorem
pure_le_nhds
modified
theorem
tendsto_const_nhds
Modified
src/topology/bounded_continuous_function.lean
Modified
src/topology/compact_open.lean
Modified
src/topology/constructions.lean
modified
theorem
map_nhds_subtype_val_eq
modified
theorem
nhds_prod_eq
modified
theorem
nhds_swap
Modified
src/topology/continuous_on.lean
modified
theorem
continuous_within_at_inter
modified
theorem
inter_mem_nhds_within
modified
theorem
mem_nhds_within_of_mem_nhds
modified
def
nhds_within
modified
theorem
nhds_within_restrict'
modified
theorem
nhds_within_univ
Modified
src/topology/dense_embedding.lean
modified
theorem
dense_inducing.comap_nhds_neq_bot
modified
theorem
dense_inducing.extend_eq
modified
theorem
dense_inducing.tendsto_comap_nhds_nhds
Modified
src/topology/instances/complex.lean
modified
theorem
complex.tendsto_inv
Modified
src/topology/instances/ennreal.lean
modified
theorem
ennreal.Icc_mem_nhds
modified
theorem
ennreal.coe_range_mem_nhds
modified
theorem
ennreal.nhds_coe
modified
theorem
ennreal.nhds_coe_coe
modified
theorem
ennreal.nhds_of_ne_top
modified
theorem
ennreal.nhds_top
modified
theorem
ennreal.nhds_zero
modified
theorem
ennreal.tendsto_of_real
Modified
src/topology/instances/nnreal.lean
modified
theorem
nnreal.tendsto_of_real
Modified
src/topology/instances/real.lean
modified
theorem
real.tendsto_inv
Modified
src/topology/list.lean
modified
theorem
nhds_list
modified
theorem
nhds_nil
Modified
src/topology/local_homeomorph.lean
Modified
src/topology/maps.lean
modified
theorem
inducing.map_nhds_eq
modified
theorem
is_open_map_iff_nhds_le
Modified
src/topology/metric_space/basic.lean
modified
theorem
metric.ball_mem_nhds
modified
theorem
metric.mem_nhds_iff
modified
theorem
metric.nhds_eq
modified
theorem
nhds_comap_dist
Modified
src/topology/metric_space/cau_seq_filter.lean
modified
theorem
ennreal.half_pow_tendsto_zero
modified
theorem
sequentially_complete.B2_lim
modified
theorem
sequentially_complete.le_nhds_cau_filter_lim
Modified
src/topology/metric_space/closeds.lean
Modified
src/topology/metric_space/emetric_space.lean
modified
theorem
emetric.ball_mem_nhds
modified
theorem
emetric.mem_nhds_iff
modified
theorem
emetric.nhds_eq
Modified
src/topology/metric_space/gromov_hausdorff.lean
Modified
src/topology/metric_space/gromov_hausdorff_realized.lean
Modified
src/topology/metric_space/lipschitz.lean
Modified
src/topology/order.lean
modified
theorem
map_nhds_induced_eq
Modified
src/topology/separation.lean
modified
theorem
compl_singleton_mem_nhds
modified
theorem
eq_of_nhds_neq_bot
modified
theorem
lim_eq
modified
theorem
lim_nhds_eq
modified
theorem
locally_compact_of_compact_nhds
modified
theorem
nhds_eq_nhds_iff
modified
theorem
nhds_is_closed
modified
theorem
nhds_le_nhds_iff
modified
theorem
t2_iff_nhds
Modified
src/topology/sequences.lean
Modified
src/topology/stone_cech.lean
modified
theorem
convergent_eqv_pure
modified
theorem
ultrafilter_comap_pure_nhds
Modified
src/topology/subset_properties.lean
modified
def
compact
Modified
src/topology/topological_fiber_bundle.lean
Modified
src/topology/uniform_space/basic.lean
modified
theorem
nhds_eq_comap_uniformity
modified
theorem
nhds_eq_uniformity
modified
theorem
tendsto_left_nhds_uniformity
modified
theorem
tendsto_right_nhds_uniformity
Modified
src/topology/uniform_space/cauchy.lean
modified
theorem
cauchy_nhds
modified
def
is_complete
Modified
src/topology/uniform_space/complete_separated.lean
Modified
src/topology/uniform_space/completion.lean
Modified
src/topology/uniform_space/pi.lean
Modified
src/topology/uniform_space/separation.lean
Modified
src/topology/uniform_space/uniform_embedding.lean