Commit 2023-05-08 00:54 2c51ddac

View on Github →

feat: port Analysis.Normed.Group.Quotient (#3457)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Group/Quotient.lean

added theorem AddSubgroup.ker_normedMk

added theorem AddSubgroup.norm_normedMk

added theorem AddSubgroup.norm_normedMk_le

added theorem AddSubgroup.norm_trivial_quotient_mk

added theorem AddSubgroup.normedMk.apply

added theorem AddSubgroup.quotient_norm_eq

added theorem AddSubgroup.surjective_normedMk

added theorem Ideal.Quotient.norm_mk_le

added theorem NormedAddGroupHom.IsQuotient.norm_le

added theorem NormedAddGroupHom.IsQuotient.norm_lift

added structure NormedAddGroupHom.IsQuotient

added theorem NormedAddGroupHom.isQuotientQuotient

added theorem NormedAddGroupHom.lift_mk

added theorem NormedAddGroupHom.lift_normNoninc

added theorem NormedAddGroupHom.lift_norm_le

added theorem NormedAddGroupHom.lift_unique

added theorem NormedAddGroupHom.norm_lift_le

added theorem QuotientAddGroup.norm_eq_infDist

added theorem QuotientAddGroup.norm_lift_apply_le

added theorem QuotientAddGroup.norm_lt_iff

added theorem QuotientAddGroup.norm_mk

added theorem Submodule.Quotient.norm_mk_le

added theorem bddBelow_image_norm

added theorem image_norm_nonempty

added theorem isGLB_quotient_norm

added theorem norm_mk_eq_zero

added theorem norm_mk_lt'

added theorem norm_mk_lt

added theorem norm_mk_nonneg

added theorem norm_mk_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_mk_le

added theorem quotient_norm_neg

added theorem quotient_norm_nonneg

added theorem quotient_norm_sub_rev

Modified Mathlib/Data/Real/ENNReal.lean

added theorem ENNReal.coe_infᵢ

added theorem ENNReal.toNNReal_infᵢ

added theorem ENNReal.toReal_infᵢ

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

added theorem Metric.infDist_eq_infᵢ