Mathlib Changelog
v3
Changelog
About
Github
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