Theorems · Definition · functional analysis
NormedAddGroupHom.comp
{V₁ : Type u_2} →
{V₂ : Type u_3} →
{V₃ : Type u_4} →
[inst : SeminormedAddCommGroup V₁] →
[inst_1 : SeminormedAddCommGroup V₂] →
[inst_2 : SeminormedAddCommGroup V₃] →
NormedAddGroupHom V₂ V₃ → NormedAddGroupHom V₁ V₂ → NormedAddGroupHom V₁ V₃The composition of continuous normed group homs.
- Defined in
- Mathlib.Analysis.Normed.Group.Hom
- Cited by
- 39 results in Mathlib
- Foundations
- Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Norm.normproof · cited by 5,413
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- AddMonoidHom.compproof · cited by 339
- NormedAddGroupHomstatement and proof · cited by 216
- NormedAddGroupHom.toAddMonoidHomproof · cited by 13
- AddMonoidHom.mkNormedAddGroupHomproof · cited by 5
Cited by45
Results whose statement or proof uses this declaration.
- NormedAddGroupHom.Equalizer.liftstatement and proof · cited by 6
- NormedAddGroupHom.comp_applystatement and proof · cited by 5
- NormedAddGroupHom.Equalizer.mapstatement and proof · cited by 5
- NormedAddGroupHom.ker.liftstatement and proof · cited by 3
- SeparationQuotient.liftNormedAddGroupHomEquivproof · cited by 2
- NormedAddGroupHom.Equalizer.liftEquivstatement and proof · cited by 2
- NormedAddGroupHom.ker_le_ker_completionstatement and proof · cited by 1
- NormedAddGroupHom.norm_comp_lestatement · cited by 1
- NormedAddGroupHom.norm_comp_le_of_lestatement · cited by 1
- NormedAddGroupHom.coe_compstatement · cited by 1
- NormedAddGroupHom.Equalizer.comm_sq₂statement and proof · cited by 1
- NormedAddGroupHom.comp_assocstatement and proof · cited by 1