Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-18 04:49 1b864c0d

View on Github →

feat(analysis/normed_group): quotients (#7603) From LTE.

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem mem_ball_0_iff

Created src/analysis/normed_space/normed_group_quotient.lean

added theorem add_subgroup.is_quotient.norm_le

added theorem add_subgroup.is_quotient.norm_lift

added structure add_subgroup.is_quotient

added theorem add_subgroup.is_quotient_quotient

added theorem add_subgroup.ker_normed_mk

added def add_subgroup.lift

added theorem add_subgroup.lift_mk

added theorem add_subgroup.lift_unique

added theorem add_subgroup.norm_normed_mk

added theorem add_subgroup.norm_normed_mk_le

added theorem add_subgroup.norm_trivial_quotient_mk

added theorem add_subgroup.normed_mk.apply

added def add_subgroup.normed_mk

added theorem add_subgroup.surjective_normed_mk

added theorem bdd_below_image_norm

added theorem image_norm_nonempty

added theorem norm_mk_lt'

added theorem norm_mk_lt

added theorem norm_mk_nonneg

added theorem norm_mk_zero

added theorem norm_zero_eq_zero

added theorem quotient_nhd_basis

added theorem quotient_norm_add_le

added theorem quotient_norm_eq_zero_iff

added theorem quotient_norm_mk_eq

added theorem quotient_norm_mk_le

added theorem quotient_norm_neg

added theorem quotient_norm_nonneg

added theorem quotient_norm_sub_rev