Mathlib Map

Theorems · Definition · functional analysis

NormedAddGroupHom.equalizer

{V : Type u_1} →
  {W : Type u_2} →
    [inst : SeminormedAddCommGroup V] →
      [inst_1 : SeminormedAddCommGroup W] → NormedAddGroupHom V W → NormedAddGroupHom V W → AddSubgroup V

The equalizer of two morphisms f g : NormedAddGroupHom V W.

Defined in
Mathlib.Analysis.Normed.Group.Hom
Cited by
14 results in Mathlib
Foundations
Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SeminormedAddCommGroupSeminormedAddCommGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NormedAddGroupHom.Equalizer.ι · cited by 7Equalizer.ιNormedAddGroupHom.Equalizer.lift · cited by 6Equalizer.liftNormedAddGroupHom.Equalizer.map · cited by 5Equalizer.mapNormedAddGroupHom.Equalizer.liftEquiv · cited by 2Equalizer.liftEquivNormedAddGroupHom.Equalizer.lift_normNoninc · cited by 1Equalizer.lift_normNonincNormedAddGroupHom.Equalizer.norm_lift_le · cited by 1Equalizer.norm_lift_leNormedAddGroupHom.Equalizer.ι_comp_lift · cited by 1Equalizer.ι_comp_liftNormedAddGroupHom.Equalizer.ι_normNoninc · cited by 1Equalizer.ι_normNonincNormedAddGroupHom.Equalizer.comp_ι_eq · cited by 0Equalizer.comp_ι_eqNormedAddGroupHom.Equalizer.liftEquiv_apply · cited by 0Equalizer.liftEquiv_applyNormedAddGroupHom.Equalizer.liftEquiv_symm_apply_coe · cited by 0Equalizer.liftEquiv_symm_…NormedAddGroupHom.Equalizer.lift_apply_coe · cited by 0Equalizer.lift_apply_coeNormedAddGroupHom.Equalizer.map_comp_map · cited by 0Equalizer.map_comp_mapNormedAddGroupHom.Equalizer.map_id · cited by 0Equalizer.map_idNormedAddGroupHom.Equalizer.map_normNoninc · cited by 0Equalizer.map_normNonincAddSubgroup · cited by 3232AddSubgroupSeminormedAddCommGroup · cited by 2671SeminormedAddCommGroupNormedAddGroupHom · cited by 216NormedAddGroupHomNormedAddGroupHom.ker · cited by 14NormedAddGroupHom.kerNormedAddGroupHom.equalizerCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by18

Results whose statement or proof uses this declaration.