Commit 2025-02-05 23:29 9d6e2ee0

View on Github →

feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and mk (#18178) Define the mk and lifts of normed spaces and normed groups by the inseparable setoid as NormedAddGroupHom, CLM, etc.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Group/Hom.lean

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

added theorem SeparationQuotient.apply_eq_apply_of_inseparable

added theorem SeparationQuotient.liftNormedAddGroupHom_normNoninc

added theorem SeparationQuotient.liftNormedAddGroupHom_norm_le

added theorem SeparationQuotient.norm_liftNormedAddGroupHom_apply_le

added theorem SeparationQuotient.norm_liftNormedAddGroupHom_le

added theorem SeparationQuotient.norm_normedMk_eq_one

added theorem SeparationQuotient.norm_normedMk_le

added theorem SeparationQuotient.normedMk_eq_zero_iff

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

added def ContinuousMonoidHom.ofClass

Modified Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean

added theorem SeparationQuotient.liftCLM_mk

added theorem SeparationQuotient.nhds_mk

Created Mathlib/Topology/Algebra/SeparationQuotient/Hom.lean

added theorem SeparationQuotient.liftContinuousCommMonoidHom_mk