Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-10 21:07 64255e25

View on Github →

chore(analysis): move some code to analysis.normed.group.basic (#9642)

Estimated changes

Created src/analysis/normed/group/basic.lean

added theorem abs_dist_sub_le_dist_add_add

added theorem abs_norm_sub_norm_le

added theorem add_mem_ball_iff_norm

added theorem add_mem_closed_ball_iff_norm

added theorem add_monoid_hom.continuous_of_bound

added theorem add_monoid_hom.isometry_iff_norm

added theorem add_monoid_hom.isometry_of_norm

added theorem add_monoid_hom.lipschitz_of_bound

added theorem add_monoid_hom.lipschitz_of_bound_nnnorm

added theorem antilipschitz_with.add_lipschitz_with

added theorem antilipschitz_with.add_sub_lipschitz_with

added theorem ball_zero_eq

added theorem bounded_iff_forall_norm_le

added theorem cauchy_seq.add

added theorem cauchy_seq_sum_of_eventually_eq

added theorem coe_neg_sphere

added theorem coe_nnnorm

added theorem coe_norm_subgroup

added theorem continuous.nnnorm

added theorem continuous.norm

added theorem continuous_at.nnnorm

added theorem continuous_at.norm

added theorem continuous_nnnorm

added theorem continuous_norm

added theorem continuous_on.nnnorm

added theorem continuous_on.norm

added theorem continuous_within_at.nnnorm

added theorem continuous_within_at.norm

added theorem controlled_sum_of_mem_closure

added theorem controlled_sum_of_mem_closure_range

added theorem dist_add_add_le

added theorem dist_add_add_le_of_le

added theorem dist_add_left

added theorem dist_add_right

added theorem dist_eq_norm'

added theorem dist_eq_norm

added theorem dist_le_norm_add_norm

added theorem dist_neg_neg

added theorem dist_norm_norm_le

added theorem dist_sub_left

added theorem dist_sub_right

added theorem dist_sub_sub_le

added theorem dist_sub_sub_le_of_le

added theorem dist_sum_sum_le

added theorem dist_sum_sum_le_of_le

added theorem dist_zero_left

added theorem dist_zero_right

added theorem edist_add_add_le

added theorem edist_eq_coe_nnnorm

added theorem edist_eq_coe_nnnorm_sub

added theorem eq_of_norm_sub_eq_zero

added theorem eq_of_norm_sub_le_zero

added theorem eventually_ne_of_tendsto_norm_at_top

added theorem filter.tendsto.nnnorm

added theorem filter.tendsto.norm

added theorem is_bounded_under_of_tendsto

added theorem is_compact.exists_bound_of_continuous_on

added theorem isometric.add_left_symm

added theorem isometric.add_left_to_equiv

added theorem isometric.add_right_apply

added theorem isometric.add_right_symm

added theorem isometric.add_right_to_equiv

added theorem isometric.coe_add_left

added theorem isometric.coe_add_right

added theorem isometric.coe_neg

added theorem isometric.neg_symm

added theorem isometric.neg_to_equiv

added theorem lipschitz_on_with.norm_sub_le

added theorem lipschitz_on_with_iff_norm_sub_le

added theorem lipschitz_with.add

added theorem lipschitz_with.neg

added theorem lipschitz_with.sub

added theorem lipschitz_with_iff_norm_sub_le

added theorem lipschitz_with_one_norm

added theorem mem_ball_iff_norm'

added theorem mem_ball_iff_norm

added theorem mem_ball_zero_iff

added theorem mem_closed_ball_iff_norm'

added theorem mem_closed_ball_iff_norm

added theorem mem_emetric_ball_zero_iff

added theorem mem_sphere_iff_norm

added theorem mem_sphere_zero_iff_norm

added theorem nat.norm_cast_le

added theorem ne_zero_of_norm_pos

added theorem nndist_add_add_le

added theorem nndist_eq_nnnorm

added theorem nndist_nnnorm_nnnorm_le

added theorem nnnorm_add_le

added theorem nnnorm_eq_zero

added theorem nnnorm_neg

added theorem nnnorm_sum_le

added theorem nnnorm_zero

added theorem nonzero_of_mem_sphere

added theorem nonzero_of_mem_unit_sphere

added theorem norm_add_le

added theorem norm_add_le_of_le

added theorem norm_eq_of_mem_sphere

added theorem norm_eq_zero

added theorem norm_eq_zero_iff'

added theorem norm_fst_le

added theorem norm_le_insert'

added theorem norm_le_insert

added theorem norm_le_norm_add_const_of_dist_le

added theorem norm_le_of_mem_closed_ball

added theorem norm_le_pi_norm

added theorem norm_le_zero_iff'

added theorem norm_le_zero_iff

added theorem norm_lt_norm_add_const_of_dist_lt

added theorem norm_lt_of_mem_ball

added theorem norm_neg

added theorem norm_nonneg

added theorem norm_of_subsingleton

added theorem norm_pos_iff'

added theorem norm_pos_iff

added theorem norm_prod_le_iff

added theorem norm_snd_le

added theorem norm_sub_eq_zero_iff

added theorem norm_sub_le

added theorem norm_sub_le_of_le

added theorem norm_sub_norm_le

added theorem norm_sub_rev

added theorem norm_sum_le

added theorem norm_sum_le_of_le

added theorem norm_zero

added theorem normed_group.cauchy_seq_iff

added theorem normed_group.core.to_semi_normed_group.core

added structure normed_group.core

added def normed_group.induced

added def normed_group.of_add_dist

added theorem normed_group.tendsto_nhds_nhds

added theorem normed_group.tendsto_nhds_zero

added theorem of_real_norm_eq_coe_nnnorm

added theorem pi_nnnorm_const

added theorem pi_nnsemi_norm_const

added theorem pi_norm_const

added theorem pi_norm_le_iff

added theorem pi_norm_lt_iff

added theorem pi_semi_norm_const

added theorem pi_semi_norm_le_iff

added theorem pi_semi_norm_lt_iff

added theorem preimage_add_ball

added theorem preimage_add_closed_ball

added theorem preimage_add_sphere

added theorem prod.nnnorm_def

added theorem prod.nnsemi_norm_def

added theorem prod.norm_def

added theorem prod.semi_norm_def

added theorem punit.norm_eq_zero

added theorem real.norm_eq_abs

added theorem semi_norm_fst_le

added theorem semi_norm_le_pi_norm

added theorem semi_norm_prod_le_iff

added theorem semi_norm_snd_le

added structure semi_normed_group.core

added def semi_normed_group.induced

added theorem semi_normed_group.mem_closure_iff

added def semi_normed_group.of_add_dist'

added def semi_normed_group.of_add_dist

added theorem squeeze_zero_norm'

added theorem squeeze_zero_norm

added theorem submodule.norm_coe

added theorem submodule.norm_mk

added theorem tendsto_iff_norm_tendsto_zero

added theorem tendsto_norm

added theorem tendsto_norm_cocompact_at_top

added theorem tendsto_norm_nhds_within_zero

added theorem tendsto_norm_sub_self

added theorem tendsto_norm_zero

added theorem tendsto_zero_iff_norm_tendsto_zero

added theorem uniform_continuous_nnnorm

added theorem uniform_continuous_norm

Modified src/analysis/normed_space/basic.lean

deleted theorem abs_dist_sub_le_dist_add_add

deleted theorem abs_norm_sub_norm_le

deleted theorem add_mem_ball_iff_norm

deleted theorem add_mem_closed_ball_iff_norm

deleted theorem add_monoid_hom.continuous_of_bound

deleted theorem add_monoid_hom.isometry_iff_norm

deleted theorem add_monoid_hom.isometry_of_norm

deleted theorem add_monoid_hom.lipschitz_of_bound

deleted theorem add_monoid_hom.lipschitz_of_bound_nnnorm

deleted theorem antilipschitz_with.add_lipschitz_with

deleted theorem antilipschitz_with.add_sub_lipschitz_with

deleted theorem ball_zero_eq

deleted theorem bounded_iff_forall_norm_le

deleted theorem cauchy_seq.add

deleted theorem cauchy_seq_sum_of_eventually_eq

deleted theorem coe_neg_sphere

deleted theorem coe_nnnorm

deleted theorem coe_norm_subgroup

deleted theorem continuous.nnnorm

deleted theorem continuous.norm

deleted theorem continuous_at.nnnorm

deleted theorem continuous_at.norm

deleted theorem continuous_nnnorm

deleted theorem continuous_norm

deleted theorem continuous_on.nnnorm

deleted theorem continuous_on.norm

deleted theorem continuous_within_at.nnnorm

deleted theorem continuous_within_at.norm

deleted theorem controlled_sum_of_mem_closure

deleted theorem controlled_sum_of_mem_closure_range

deleted theorem dist_add_add_le

deleted theorem dist_add_add_le_of_le

deleted theorem dist_add_left

deleted theorem dist_add_right

deleted theorem dist_eq_norm'

deleted theorem dist_eq_norm

deleted theorem dist_le_norm_add_norm

deleted theorem dist_neg_neg

deleted theorem dist_norm_norm_le

deleted theorem dist_sub_left

deleted theorem dist_sub_right

deleted theorem dist_sub_sub_le

deleted theorem dist_sub_sub_le_of_le

deleted theorem dist_sum_sum_le

deleted theorem dist_sum_sum_le_of_le

deleted theorem dist_zero_left

deleted theorem dist_zero_right

deleted theorem edist_add_add_le

deleted theorem edist_eq_coe_nnnorm

deleted theorem edist_eq_coe_nnnorm_sub

deleted theorem eq_of_norm_sub_eq_zero

deleted theorem eq_of_norm_sub_le_zero

deleted theorem eventually_ne_of_tendsto_norm_at_top

deleted theorem filter.tendsto.nnnorm

deleted theorem filter.tendsto.norm

deleted theorem is_bounded_under_of_tendsto

deleted theorem is_compact.exists_bound_of_continuous_on

deleted theorem isometric.add_left_symm

deleted theorem isometric.add_left_to_equiv

deleted theorem isometric.add_right_apply

deleted theorem isometric.add_right_symm

deleted theorem isometric.add_right_to_equiv

deleted theorem isometric.coe_add_left

deleted theorem isometric.coe_add_right

deleted theorem isometric.coe_neg

deleted theorem isometric.neg_symm

deleted theorem isometric.neg_to_equiv

deleted theorem lipschitz_on_with.norm_sub_le

deleted theorem lipschitz_on_with_iff_norm_sub_le

deleted theorem lipschitz_with.add

deleted theorem lipschitz_with.neg

deleted theorem lipschitz_with.sub

deleted theorem lipschitz_with_iff_norm_sub_le

deleted theorem lipschitz_with_one_norm

deleted theorem mem_ball_iff_norm'

deleted theorem mem_ball_iff_norm

deleted theorem mem_ball_zero_iff

deleted theorem mem_closed_ball_iff_norm'

deleted theorem mem_closed_ball_iff_norm

deleted theorem mem_emetric_ball_zero_iff

deleted theorem mem_sphere_iff_norm

deleted theorem mem_sphere_zero_iff_norm

deleted theorem nat.norm_cast_le

deleted theorem ne_zero_of_norm_pos

deleted theorem nndist_add_add_le

deleted theorem nndist_eq_nnnorm

deleted theorem nndist_nnnorm_nnnorm_le

deleted theorem nnnorm_add_le

deleted theorem nnnorm_eq_zero

deleted theorem nnnorm_neg

deleted theorem nnnorm_sum_le

deleted theorem nnnorm_zero

deleted theorem nonzero_of_mem_sphere

deleted theorem nonzero_of_mem_unit_sphere

deleted theorem norm_add_le

deleted theorem norm_add_le_of_le

deleted theorem norm_eq_of_mem_sphere

deleted theorem norm_eq_zero

deleted theorem norm_eq_zero_iff'

deleted theorem norm_fst_le

deleted theorem norm_le_insert'

deleted theorem norm_le_insert

deleted theorem norm_le_norm_add_const_of_dist_le

deleted theorem norm_le_of_mem_closed_ball

deleted theorem norm_le_pi_norm

deleted theorem norm_le_zero_iff'

deleted theorem norm_le_zero_iff

deleted theorem norm_lt_norm_add_const_of_dist_lt

deleted theorem norm_lt_of_mem_ball

deleted theorem norm_neg

deleted theorem norm_nonneg

deleted theorem norm_of_subsingleton

deleted theorem norm_pos_iff'

deleted theorem norm_pos_iff

deleted theorem norm_prod_le_iff

deleted theorem norm_snd_le

deleted theorem norm_sub_eq_zero_iff

deleted theorem norm_sub_le

deleted theorem norm_sub_le_of_le

deleted theorem norm_sub_norm_le

deleted theorem norm_sub_rev

deleted theorem norm_sum_le

deleted theorem norm_sum_le_of_le

deleted theorem norm_zero

deleted theorem normed_group.cauchy_seq_iff

deleted theorem normed_group.core.to_semi_normed_group.core

deleted structure normed_group.core

deleted def normed_group.induced

deleted def normed_group.of_add_dist

deleted theorem normed_group.tendsto_nhds_nhds

deleted theorem normed_group.tendsto_nhds_zero

deleted theorem of_real_norm_eq_coe_nnnorm

deleted theorem pi_nnnorm_const

deleted theorem pi_nnsemi_norm_const

deleted theorem pi_norm_const

deleted theorem pi_norm_le_iff

deleted theorem pi_norm_lt_iff

deleted theorem pi_semi_norm_const

deleted theorem pi_semi_norm_le_iff

deleted theorem pi_semi_norm_lt_iff

deleted theorem preimage_add_ball

deleted theorem preimage_add_closed_ball

deleted theorem preimage_add_sphere

deleted theorem prod.nnnorm_def

deleted theorem prod.nnsemi_norm_def

deleted theorem prod.norm_def

deleted theorem prod.semi_norm_def

deleted theorem punit.norm_eq_zero

deleted theorem real.norm_eq_abs

deleted theorem semi_norm_fst_le

deleted theorem semi_norm_le_pi_norm

deleted theorem semi_norm_prod_le_iff

deleted theorem semi_norm_snd_le

deleted structure semi_normed_group.core

deleted def semi_normed_group.induced

deleted theorem semi_normed_group.mem_closure_iff

deleted def semi_normed_group.of_add_dist'

deleted def semi_normed_group.of_add_dist

deleted theorem squeeze_zero_norm'

deleted theorem squeeze_zero_norm

deleted theorem submodule.norm_coe

deleted theorem submodule.norm_mk

deleted theorem tendsto_iff_norm_tendsto_zero

deleted theorem tendsto_norm

deleted theorem tendsto_norm_cocompact_at_top

deleted theorem tendsto_norm_nhds_within_zero

deleted theorem tendsto_norm_sub_self

deleted theorem tendsto_norm_zero

deleted theorem tendsto_zero_iff_norm_tendsto_zero

deleted theorem uniform_continuous_nnnorm

deleted theorem uniform_continuous_norm