Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-08 09:28 f5d73bdd

View on Github →

feat(analysis/topology/continuity): add some variations

Estimated changes

Created analysis/metric_space.lean

added theorem abs_dist

added theorem abs_dist_sub_le

added def ball

added theorem ball_disjoint

added theorem ball_disjoint_same

added theorem ball_eq_empty_iff_nonpos

added theorem ball_half_subset

added theorem ball_mem_nhds

added theorem ball_subset

added theorem ball_subset_ball

added theorem ball_subset_closed_ball

added theorem cauchy_of_metric

added theorem cauchy_seq_metric'

added theorem cauchy_seq_metric

added def closed_ball

added theorem continuous_dist'

added theorem continuous_dist

added theorem continuous_of_metric

added theorem continuous_topo_metric

added theorem countable_closure_of_compact

added theorem dist_comm

added theorem dist_eq_edist

added theorem dist_eq_nndist

added theorem dist_eq_zero

added theorem dist_le_zero

added theorem dist_mem_uniformity

added theorem dist_nonneg

added theorem dist_pi_def

added theorem dist_pos

added theorem dist_self

added theorem dist_triangle

added theorem dist_triangle_left

added theorem dist_triangle_right

added theorem edist_dist

added theorem edist_eq_dist

added theorem edist_eq_nndist

added theorem edist_ne_top

added theorem eq_of_dist_eq_zero

added theorem eq_of_forall_dist_le

added theorem eq_of_nndist_eq_zero

added theorem exists_ball_subset_ball

added theorem exists_delta_of_continuous

added theorem finite_cover_balls_of_compact

added theorem is_closed_ball

added theorem is_open_ball

added theorem is_open_metric

added theorem lebesgue_number_lemma_of_metric

added theorem lebesgue_number_lemma_of_metric_sUnion

added theorem mem_ball'

added theorem mem_ball

added theorem mem_ball_comm

added theorem mem_ball_self

added theorem mem_closed_ball

added theorem mem_closure_iff'

added theorem mem_nhds_iff_metric

added theorem mem_uniformity_dist

added theorem mem_uniformity_dist_edist

added def metric_space.induced

added def metric_space.replace_uniformity

added def metric_space.uniform_space_of_dist

added theorem nhds_comap_dist

added theorem nhds_eq_metric

added def nndist

added theorem nndist_comm

added theorem nndist_eq_dist

added theorem nndist_eq_edist

added theorem nndist_eq_zero

added theorem nndist_self

added theorem nndist_triangle

added theorem nndist_triangle_left

added theorem nndist_triangle_right

added theorem pos_of_mem_ball

added theorem real.dist_0_eq_abs

added theorem real.dist_eq

added theorem second_countable_of_separable_metric_space

added theorem subtype.dist_eq

added theorem swap_dist

added theorem tendsto_at_top_metric

added theorem tendsto_dist

added theorem tendsto_iff_dist_tendsto_zero

added theorem tendsto_nhds_of_metric

added theorem tendsto_nhds_topo_metric

added theorem totally_bounded_of_metric

added theorem uniform_continuous_dist'

added theorem uniform_continuous_dist

added theorem uniform_continuous_of_metric

added theorem uniform_embedding_of_metric

added theorem uniformity_dist'

added theorem uniformity_dist

added theorem uniformity_edist'

added theorem uniformity_edist

added theorem zero_eq_dist

added theorem zero_eq_nndist

Created data/real/cau_seq_filter.lean

added theorem cau_seq_iff_cauchy_seq

added theorem cauchy_of_filter_cauchy

added theorem complete_of_cauchy_seq_tendsto

added theorem filter_cauchy_of_cauchy

added theorem sequentially_complete.cauchy_seq_of_dist_tendsto_0

added theorem sequentially_complete.le_nhds_cau_filter_lim

added theorem sequentially_complete.mono_of_mono_succ

added theorem sequentially_complete.seq_of_cau_filter_is_cauchy'

added theorem sequentially_complete.seq_of_cau_filter_is_cauchy

added theorem sequentially_complete.seq_of_cau_filter_mem_set_seq

added def sequentially_complete.set_seq_of_cau_filter

added theorem sequentially_complete.set_seq_of_cau_filter_inhabited

added theorem sequentially_complete.set_seq_of_cau_filter_mem_sets

added theorem sequentially_complete.set_seq_of_cau_filter_monotone'

added theorem sequentially_complete.set_seq_of_cau_filter_monotone

added theorem sequentially_complete.set_seq_of_cau_filter_spec

added theorem sequentially_complete.tendsto_div

added theorem tendsto_limit

Modified src/analysis/exponential.lean

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/bounded_linear_maps.lean

Modified src/data/padics/hensel.lean

Modified src/topology/algebra/group.lean

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/algebra/topological_structures.lean

Modified src/topology/compact_open.lean

Modified src/topology/continuity.lean

added def continuous_at

modified theorem continuous_at_iff_ultrafilter

added theorem continuous_at_subtype_val

added def continuous_at_within

added theorem continuous_at_within_iff_continuous_at_restrict

added theorem continuous_at_within_iff_ptendsto_res

added theorem continuous_at_within_univ

added theorem continuous_iff_continuous_at

deleted theorem continuous_iff_tendsto

added def continuous_on

added theorem continuous_on_iff'

added theorem continuous_on_iff

added theorem continuous_on_iff_continuous_restrict

added theorem list.continuous_at_length

deleted theorem list.tendsto_length

added theorem open_dom_of_pcontinuous

added def pcontinuous

added theorem pcontinuous_iff'

deleted theorem tendsto_subtype_val

added theorem vector.continuous_at_remove_nth

deleted theorem vector.tendsto_remove_nth

Modified src/topology/instances/complex.lean

Modified src/topology/instances/ennreal.lean

Modified src/topology/instances/nnreal.lean

Modified src/topology/instances/real.lean

Modified src/topology/uniform_space/basic.lean

Modified src/topology/uniform_space/completion.lean