Hom

📁 Source: Mathlib/Analysis/Normed/Group/Hom.lean

Statistics

Metric	Count
Definitions `mkNormedAddGroupHom`, `mkNormedAddGroupHom'`, `NormedAddGroupHom`, `liftEquiv`, `map`, `ι`, `NormNoninc`, `SurjectiveOnWith`, `add`, `coeAddHom`, `comp`, `compHom`, `distribMulAction`, `equalizer`, `funLike`, `hasOpNorm`, `id`, `incl`, `inhabited`, `ker`, `neg`, `nsmul`, `ofLipschitz`, `opNorm`, `range`, `smul`, `sub`, `toAddCommGroup`, `toAddMonoidHom`, `toFun`, `toNormedAddCommGroup`, `toSeminormedAddCommGroup`, `zero`, `zsmul`	34
Theorems `mkNormedAddGroupHom_norm_le`, `mkNormedAddGroupHom_norm_le'`, `comm_sq₂`, `comp_ι_eq`, `liftEquiv_apply`, `liftEquiv_symm_apply_coe`, `lift_apply_coe`, `lift_normNoninc`, `map_comp_map`, `map_id`, `map_normNoninc`, `norm_lift_le`, `norm_map_le`, `ι_comp_lift`, `ι_comp_map`, `ι_normNoninc`, `comp`, `id`, `neg_iff`, `normNoninc_iff_norm_le_one`, `zero`, `exists_pos`, `mono`, `surjOn`, `add_apply`, `antilipschitz_of_norm_ge`, `bound'`, `bounds_bddBelow`, `bounds_nonempty`, `coeAddHom_apply`, `coe_add`, `coe_comp`, `coe_id`, `coe_inj`, `coe_inj_iff`, `coe_injective`, `coe_ker`, `coe_mk`, `coe_mkNormedAddGroupHom`, `coe_mkNormedAddGroupHom'`, `coe_neg`, `coe_nsmul`, `coe_smul`, `coe_sub`, `coe_sum`, `coe_toAddMonoidHom`, `coe_zero`, `coe_zsmul`, `comp_apply`, `comp_assoc`, `comp_range`, `comp_zero`, `continuous`, `ext`, `ext_iff`, `id_apply`, `incl_apply`, `incl_range`, `instContinuousMapClass`, `isCentralScalar`, `isClosed_ker`, `isScalarTower`, `isometry_comp`, `isometry_id`, `incl_comp_lift`, `lift_apply_coe`, `ker_zero`, `le_of_opNorm_le`, `le_opNorm`, `le_opNorm_of_le`, `lipschitz`, `map_add'`, `mem_ker`, `mem_range`, `mem_range_self`, `mkNormedAddGroupHom_norm_le`, `mkNormedAddGroupHom_norm_le'`, `mk_toAddMonoidHom`, `neg_apply`, `normNoninc_of_isometry`, `norm_comp_le`, `norm_comp_le_of_le`, `norm_comp_le_of_le'`, `norm_def`, `norm_eq_of_isometry`, `norm_id`, `norm_id_le`, `norm_id_of_nontrivial_seminorm`, `norm_incl`, `nsmul_apply`, `ofLipschitz_norm_le`, `opNorm_add_le`, `opNorm_eq_of_bounds`, `opNorm_le_bound`, `opNorm_le_of_lipschitz`, `opNorm_neg`, `opNorm_nonneg`, `opNorm_zero`, `opNorm_zero_iff`, `range_comp_incl_top`, `ratio_le_opNorm`, `smulCommClass`, `smul_apply`, `sub_apply`, `sum_apply`, `toAddMonoidHomClass`, `toAddMonoidHom_injective`, `toFun_eq_coe`, `uniformContinuous`, `zero_apply`, `zero_comp`, `zsmul_apply`, `exists_pos_bound_of_bound`	113
Total	147

AddMonoidHom

Definitions

Name	Category	Theorems
`mkNormedAddGroupHom` 📖	CompOp	5 math math: `NormedAddGroupHom.mkNormedAddGroupHom_norm_le`, `NormedAddGroupHom.coe_mkNormedAddGroupHom`, `NormedAddGroupHom.mkNormedAddGroupHom_norm_le'`, `mkNormedAddGroupHom_norm_le`, `mkNormedAddGroupHom_norm_le'`
`mkNormedAddGroupHom'` 📖	CompOp	1 math math: `NormedAddGroupHom.coe_mkNormedAddGroupHom'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mkNormedAddGroupHom_norm_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instFunLike` `Real.instMul`	`NormedAddGroupHom` `NormedAddGroupHom.hasOpNorm` `mkNormedAddGroupHom`	—	`NormedAddGroupHom.mkNormedAddGroupHom_norm_le`
`mkNormedAddGroupHom_norm_le'` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instFunLike` `Real.instMul`	`NormedAddGroupHom` `NormedAddGroupHom.hasOpNorm` `mkNormedAddGroupHom` `Real.instMax` `Real.instZero`	—	`NormedAddGroupHom.mkNormedAddGroupHom_norm_le'`

NormedAddGroupHom

Definitions

Name	Category	Theorems
`NormNoninc` 📖	MathDef	21 math math: `SemiNormedGrp₁.comp_apply`, `Equalizer.ι_normNoninc`, `SemiNormedGrp₁.coe_id`, `NormNoninc.normNoninc_iff_norm_le_one`, `SemiNormedGrp₁.mkHom_hom`, `SemiNormedGrp₁.hom_comp`, `NormNoninc.zero`, `SemiNormedGrp₁.hom_id`, `SemiNormedGrp₁.Hom.normNoninc`, `NormNoninc.id`, `SemiNormedGrp₁.iso_isometry`, `SemiNormedGrp₁.coe_comp`, `SemiNormedGrp₁.ext_iff`, `SemiNormedGrp₁.instAddMonoidHomClassSubtypeNormedAddGroupHomCarrierNormNoninc`, `SemiNormedGrp₁.zero_apply`, `SemiNormedGrp₁.id_apply`, `SemiNormedGrp.normNoninc_explicitCokernelπ`, `normNoninc_of_isometry`, `SemiNormedGrp₁.hom_inv_apply`, `NormNoninc.neg_iff`, `SemiNormedGrp₁.inv_hom_apply`
`SurjectiveOnWith` 📖	MathDef	1 math math: `controlled_closure_range_of_complete`
`add` 📖	CompOp	5 math math: `add_apply`, `SemiNormedGrp.hom_add`, `completion_add`, `opNorm_add_le`, `coe_add`
`coeAddHom` 📖	CompOp	1 math math: `coeAddHom_apply`
`comp` 📖	CompOp	24 math math: `norm_comp_le`, `SemiNormedGrp₁.hom_comp`, `comp_assoc`, `norm_comp_le_of_le`, `coe_comp`, `Equalizer.liftEquiv_apply`, `range_comp_incl_top`, `comp_range`, `SemiNormedGrp.hom_comp`, `comp_apply`, `ker_completion`, `completion_toCompl`, `norm_comp_le_of_le'`, `Equalizer.comp_ι_eq`, `ker_le_ker_completion`, `completion_comp`, `Equalizer.map_id`, `zero_comp`, `NormNoninc.comp`, `SemiNormedGrp.ofHom_comp`, `SeparationQuotient.liftNormedAddGroupHomEquiv_symm_apply_coe`, `comp_zero`, `Equalizer.liftEquiv_symm_apply_coe`, `isometry_comp`
`compHom` 📖	CompOp	—
`distribMulAction` 📖	CompOp	—
`equalizer` 📖	CompOp	12 math math: `Equalizer.ι_normNoninc`, `Equalizer.map_normNoninc`, `Equalizer.liftEquiv_apply`, `Equalizer.ι_comp_map`, `Equalizer.lift_normNoninc`, `Equalizer.ι_comp_lift`, `Equalizer.lift_apply_coe`, `Equalizer.map_comp_map`, `Equalizer.comp_ι_eq`, `Equalizer.map_id`, `Equalizer.norm_lift_le`, `Equalizer.liftEquiv_symm_apply_coe`
`funLike` 📖	CompOp	89 math math: `SemiNormedGrp₁.comp_apply`, `completion_def`, `coe_toAddMonoidHom`, `SemiNormedGrp₁.coe_id`, `SemiNormedGrp.explicitCokernelπ_desc_apply`, `NormedAddCommGroup.norm_toCompl`, `coe_mkNormedAddGroupHom'`, `instContinuousMapClass`, `SemiNormedGrp.coe_comp`, `smul_apply`, `add_apply`, `toFun_eq_coe`, `extension_coe_to_fun`, `IsQuotient.norm_le`, `neg_apply`, `SemiNormedGrp.ext_iff`, `SemiNormedGrp.zero_apply`, `coe_mkNormedAddGroupHom`, `completion_coe`, `isometry_id`, `NormedAddCommGroup.denseRange_toCompl`, `le_of_opNorm_le`, `SemiNormedGrp.id_apply`, `mem_ker`, `coe_comp`, `le_opNorm_of_le`, `SemiNormedGrp.completion.norm_incl_eq`, `coe_nsmul`, `extension_coe`, `zero_apply`, `uniformContinuous`, `IsQuotient.norm_lift`, `sub_apply`, `ratio_le_opNorm`, `SemiNormedGrp.inv_hom_apply`, `completion_coe_to_fun`, `SemiNormedGrp₁.iso_isometry`, `SemiNormedGrp₁.mkHom_apply`, `coe_neg`, `SemiNormedGrp.explicitCokernelπ_apply_dom_eq_zero`, `SemiNormedGrp₁.coe_comp`, `SemiNormedGrp.explicitCokernelπ_surjective`, `bound`, `incl_apply`, `id_apply`, `coe_sum`, `le_opNorm`, `comp_apply`, `SurjectiveOnWith.surjOn`, `Equalizer.lift_apply_coe`, `SemiNormedGrp₁.ext_iff`, `AddSubgroup.surjective_normedMk`, `coe_sub`, `SemiNormedGrp.ofHom_apply`, `IsQuotient.norm`, `SemiNormedGrp₁.zero_apply`, `coe_ker`, `SemiNormedGrp₁.id_apply`, `toAddMonoidHomClass`, `mem_range_self`, `SeparationQuotient.normedMk_apply`, `SemiNormedGrp.coe_id`, `NormedAddCommGroup.toCompl_apply`, `SemiNormedGrp₁.hom_inv_apply`, `lipschitz`, `coe_id`, `nsmul_apply`, `coeAddHom_apply`, `extension_def`, `SemiNormedGrp.comp_apply`, `ker.lift_apply_coe`, `completion_coe'`, `coe_mk`, `mem_range`, `coe_add`, `sum_apply`, `IsQuotient.surjective`, `coe_smul`, `coe_inj_iff`, `SemiNormedGrp.iso_isometry_of_normNoninc`, `AddSubgroup.normedMk.apply`, `coe_zero`, `ext_iff`, `zsmul_apply`, `SemiNormedGrp.hom_inv_apply`, `SemiNormedGrp₁.inv_hom_apply`, `continuous`, `norm_incl`, `coe_zsmul`
`hasOpNorm` 📖	CompOp	33 math math: `norm_id_of_nontrivial_seminorm`, `norm_comp_le`, `AddSubgroup.norm_normedMk_le`, `SeparationQuotient.norm_liftNormedAddGroupHom_apply_le`, `NormNoninc.normNoninc_iff_norm_le_one`, `norm_id_le`, `opNorm_le_of_lipschitz`, `AddSubgroup.norm_trivial_quotient_mk`, `norm_completion`, `SeparationQuotient.norm_normedMk_eq_one`, `SeparationQuotient.norm_normedMk_le`, `mkNormedAddGroupHom_norm_le`, `le_opNorm_of_le`, `mkNormedAddGroupHom_norm_le'`, `opNorm_eq_of_bounds`, `opNorm_add_le`, `ratio_le_opNorm`, `opNorm_le_bound`, `opNorm_zero_iff`, `SeparationQuotient.norm_liftNormedAddGroupHom_le`, `le_opNorm`, `QuotientAddGroup.norm_lift_apply_le`, `ofLipschitz_norm_le`, `AddMonoidHom.mkNormedAddGroupHom_norm_le`, `opNorm_neg`, `opNorm_nonneg`, `norm_lift_le`, `lipschitz`, `AddSubgroup.norm_normedMk`, `AddMonoidHom.mkNormedAddGroupHom_norm_le'`, `norm_def`, `opNorm_zero`, `norm_id`
`id` 📖	CompOp	13 math math: `norm_id_of_nontrivial_seminorm`, `norm_id_le`, `SemiNormedGrp.hom_id`, `SemiNormedGrp₁.hom_id`, `isometry_id`, `NormNoninc.id`, `id_apply`, `SemiNormedGrp₁.mkHom_id`, `coe_id`, `Equalizer.map_id`, `SemiNormedGrp.ofHom_id`, `completion_id`, `norm_id`
`incl` 📖	CompOp	7 math math: `incl_range`, `range_comp_incl_top`, `incl_apply`, `ker_completion`, `ker.incl_comp_lift`, `ker_le_ker_completion`, `norm_incl`
`inhabited` 📖	CompOp	—
`ker` 📖	CompOp	10 math math: `mem_ker`, `isClosed_ker`, `ker_completion`, `AddSubgroup.ker_normedMk`, `IsQuotient.norm`, `coe_ker`, `ker.incl_comp_lift`, `ker_le_ker_completion`, `ker.lift_apply_coe`, `ker_zero`
`neg` 📖	CompOp	6 math math: `neg_apply`, `SemiNormedGrp.hom_neg`, `coe_neg`, `opNorm_neg`, `completion_neg`, `NormNoninc.neg_iff`
`nsmul` 📖	CompOp	3 math math: `coe_nsmul`, `nsmul_apply`, `SemiNormedGrp.hom_nsum`
`ofLipschitz` 📖	CompOp	1 math math: `ofLipschitz_norm_le`
`opNorm` 📖	CompOp	—
`range` 📖	CompOp	8 math math: `incl_range`, `BoundedContinuousFunction.range_toLpHom`, `range_comp_incl_top`, `comp_range`, `controlled_closure_range_of_complete`, `mem_range_self`, `ker_le_ker_completion`, `mem_range`
`smul` 📖	CompOp	5 math math: `smulCommClass`, `smul_apply`, `isCentralScalar`, `isScalarTower`, `coe_smul`
`sub` 📖	CompOp	4 math math: `SemiNormedGrp.hom_sub`, `completion_sub`, `sub_apply`, `coe_sub`
`toAddCommGroup` 📖	CompOp	2 math math: `coe_sum`, `sum_apply`
`toAddMonoidHom` 📖	CompOp	5 math math: `coe_toAddMonoidHom`, `mk_toAddMonoidHom`, `comp_range`, `toAddMonoidHom_injective`, `QuotientAddGroup.norm_lift_apply_le`
`toFun` 📖	CompOp	4 math math: `toFun_eq_coe`, `map_add'`, `bound'`, `coe_injective`
`toNormedAddCommGroup` 📖	CompOp	1 math math: `normedAddGroupHomCompletionHom_apply`
`toSeminormedAddCommGroup` 📖	CompOp	2 math math: `normedAddGroupHomCompletionHom_apply`, `coeAddHom_apply`
`zero` 📖	CompOp	11 math math: `zero_completion`, `NormNoninc.zero`, `zero_apply`, `SeparationQuotient.normedMk_eq_zero_iff`, `opNorm_zero_iff`, `SemiNormedGrp.hom_zero`, `zero_comp`, `opNorm_zero`, `ker_zero`, `coe_zero`, `comp_zero`
`zsmul` 📖	CompOp	3 math math: `zsmul_apply`, `SemiNormedGrp.hom_zsum`, `coe_zsmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`antilipschitz_of_norm_ge` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul` `NNReal.toReal` `DFunLike.coe` `NormedAddGroupHom` `funLike`	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`AntilipschitzWith.of_le_mul_dist` `dist_eq_norm` `map_sub` `toAddMonoidHomClass`
`bound'` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `toFun` `Real.instMul`	—	—
`bounds_bddBelow` 📖	mathematical	—	`BddBelow` `Real` `Real.instLE` `setOf` `Real.instZero`	—	—
`bounds_nonempty` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `setOf` `Real.instLE` `Real.instZero`	—	`bound` `le_of_lt`
`coeAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `NormedAddGroupHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `toSeminormedAddCommGroup` `Pi.addZeroClass` `AddMonoidHom.instFunLike` `coeAddHom` `funLike`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `add` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `comp`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `id`	—	—
`coe_inj` 📖	—	`DFunLike.coe` `NormedAddGroupHom` `funLike`	—	—	—
`coe_inj_iff` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike`	—	—
`coe_injective` 📖	mathematical	—	`NormedAddGroupHom` `toFun`	—	—
`coe_ker` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddSubgroup.instSetLike` `ker` `Set.preimage` `DFunLike.coe` `NormedAddGroupHom` `funLike` `Set` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`coe_mk` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul`	`DFunLike.coe` `NormedAddGroupHom` `funLike`	—	—
`coe_mkNormedAddGroupHom` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddMonoidHom.instFunLike` `Real.instMul`	`NormedAddGroupHom` `funLike` `AddMonoidHom.mkNormedAddGroupHom`	—	—
`coe_mkNormedAddGroupHom'` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `AddMonoidHom.instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`NormedAddGroupHom` `funLike` `AddMonoidHom.mkNormedAddGroupHom'`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `neg` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`coe_nsmul` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `nsmul` `AddMonoid.toNatSMul` `Pi.addMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `smul` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `sub` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	—
`coe_sum` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `Finset.sum` `AddCommGroup.toAddCommMonoid` `toAddCommGroup` `Pi.addCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`coe_toAddMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddMonoidHom.instFunLike` `toAddMonoidHom` `NormedAddGroupHom` `funLike`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `zero` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`coe_zsmul` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `zsmul` `SubNegMonoid.toZSMul` `Pi.subNegMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	`ext`
`comp_range` 📖	mathematical	—	`range` `comp` `AddSubgroup.map` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `toAddMonoidHom`	—	`AddMonoidHom.map_range`
`comp_zero` 📖	mathematical	—	`comp` `NormedAddGroupHom` `zero`	—	`ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `toAddMonoidHomClass`
`continuous` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `NormedAddGroupHom` `funLike`	—	`UniformContinuous.continuous` `uniformContinuous`
`ext` 📖	—	`DFunLike.coe` `NormedAddGroupHom` `funLike`	—	—	—
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `id`	—	—
`incl_apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.seminormedAddCommGroup` `funLike` `incl`	—	—
`incl_range` 📖	mathematical	—	`range` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.seminormedAddCommGroup` `incl`	—	`AddSubgroup.ext`
`instContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass` `NormedAddGroupHom` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `funLike`	—	`continuous`
`isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `NormedAddGroupHom` `smul` `MulOpposite` `MulOpposite.instMonoidWithZero` `MulOpposite.instPseudoMetricSpace` `IsBoundedSMul.op` `SeminormedAddCommGroup.toPseudoMetricSpace` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid`	—	`IsBoundedSMul.op` `ext` `IsCentralScalar.op_smul_eq_smul`
`isClosed_ker` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SetLike.coe` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddSubgroup.instSetLike` `ker` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsClosed.preimage` `continuous` `T1Space.t1` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `coe_ker`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `NormedAddGroupHom` `smul`	—	`ext` `smul_assoc`
`isometry_comp` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `NormedAddGroupHom` `funLike`	`comp`	—	`Isometry.comp`
`isometry_id` 📖	mathematical	—	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `NormedAddGroupHom` `funLike` `id`	—	`isometry_id`
`ker_zero` 📖	mathematical	—	`ker` `NormedAddGroupHom` `zero` `Top.top` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddSubgroup.instTop`	—	`AddSubgroup.ext`
`le_of_opNorm_le` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedAddGroupHom` `hasOpNorm`	`SeminormedAddCommGroup.toNorm` `DFunLike.coe` `funLike` `Real.instMul`	—	`LE.le.trans` `le_opNorm` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_nonneg`
`le_opNorm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `NormedAddGroupHom` `funLike` `Real.instMul` `hasOpNorm`	—	`bound` `MulZeroClass.mul_zero` `lt_of_le_of_ne` `norm_nonneg` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `le_csInf` `bounds_nonempty`
`le_opNorm_of_le` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`DFunLike.coe` `NormedAddGroupHom` `funLike` `Real.instMul` `hasOpNorm`	—	`le_trans` `le_opNorm` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `opNorm_nonneg`
`lipschitz` 📖	mathematical	—	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instLE` `Real.instZero` `Norm.norm` `NormedAddGroupHom` `hasOpNorm` `opNorm_nonneg` `DFunLike.coe` `funLike`	—	`LipschitzWith.of_dist_le_mul` `opNorm_nonneg` `dist_eq_norm` `map_sub` `toAddMonoidHomClass` `le_opNorm`
`map_add'` 📖	mathematical	—	`toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`mem_ker` 📖	mathematical	—	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `ker` `DFunLike.coe` `NormedAddGroupHom` `funLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`ker.eq_1` `AddMonoidHom.mem_ker` `coe_toAddMonoidHom`
`mem_range` 📖	mathematical	—	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `range` `DFunLike.coe` `NormedAddGroupHom` `funLike`	—	—
`mem_range_self` 📖	mathematical	—	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `range` `DFunLike.coe` `NormedAddGroupHom` `funLike`	—	—
`mkNormedAddGroupHom_norm_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddMonoidHom.instFunLike` `Real.instMul`	`NormedAddGroupHom` `hasOpNorm` `AddMonoidHom.mkNormedAddGroupHom`	—	`opNorm_le_bound`
`mkNormedAddGroupHom_norm_le'` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddMonoidHom.instFunLike` `Real.instMul`	`NormedAddGroupHom` `hasOpNorm` `AddMonoidHom.mkNormedAddGroupHom` `Real.instMax` `Real.instZero`	—	`opNorm_le_bound` `le_max_right` `LE.le.trans` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `le_max_left` `norm_nonneg`
`mk_toAddMonoidHom` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul`	`toAddMonoidHom` `AddMonoidHom.mk'` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`normNoninc_of_isometry` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `NormedAddGroupHom` `funLike`	`NormNoninc`	—	`le_of_eq` `norm_eq_of_isometry`
`norm_comp_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddGroupHom` `hasOpNorm` `comp` `Real.instMul`	—	`mkNormedAddGroupHom_norm_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg`
`norm_comp_le_of_le` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedAddGroupHom` `hasOpNorm`	`comp` `Real.instMul`	—	`le_trans` `norm_comp_le` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `norm_nonneg`
`norm_comp_le_of_le'` 📖	mathematical	`Real` `Real.instMul` `Real.instLE` `Norm.norm` `NormedAddGroupHom` `hasOpNorm`	`comp`	—	`norm_comp_le_of_le`
`norm_def` 📖	mathematical	—	`Norm.norm` `NormedAddGroupHom` `hasOpNorm` `InfSet.sInf` `Real` `Real.instInfSet` `setOf` `Real.instLE` `Real.instZero`	—	—
`norm_eq_of_isometry` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `NormedAddGroupHom` `funLike`	`Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`AddMonoidHomClass.isometry_iff_norm` `toAddMonoidHomClass`
`norm_id` 📖	mathematical	—	`Norm.norm` `NormedAddGroupHom` `hasOpNorm` `id` `Real` `Real.instOne`	—	`le_antisymm` `norm_id_le` `exists_norm_ne_zero` `ratio_le_opNorm` `div_self` `id_apply`
`norm_id_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddGroupHom` `hasOpNorm` `id` `Real.instOne`	—	`opNorm_le_bound` `zero_le_one` `Real.instZeroLEOneClass` `one_mul`
`norm_id_of_nontrivial_seminorm` 📖	mathematical	—	`Norm.norm` `NormedAddGroupHom` `hasOpNorm` `id` `Real` `Real.instOne`	—	`NontrivialTopology.of_exists_norm_ne_zero` `norm_id`
`norm_incl` 📖	mathematical	—	`Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `NormedAddGroupHom` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.seminormedAddCommGroup` `funLike` `incl`	—	—
`nsmul_apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `nsmul` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	—
`ofLipschitz_norm_le` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddMonoidHom.instFunLike`	`Real` `Real.instLE` `Norm.norm` `NormedAddGroupHom` `hasOpNorm` `ofLipschitz` `NNReal.toReal`	—	`mkNormedAddGroupHom_norm_le` `NNReal.coe_nonneg`
`opNorm_add_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddGroupHom` `hasOpNorm` `add` `Real.instAdd`	—	`mkNormedAddGroupHom_norm_le` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `opNorm_nonneg`
`opNorm_eq_of_bounds` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `NormedAddGroupHom` `funLike` `Real.instMul`	`hasOpNorm`	—	`le_antisymm` `opNorm_le_bound` `le_csInf_iff` `bounds_bddBelow`
`opNorm_le_bound` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `NormedAddGroupHom` `funLike` `Real.instMul`	`hasOpNorm`	—	`csInf_le` `bounds_bddBelow`
`opNorm_le_of_lipschitz` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `NormedAddGroupHom` `funLike`	`Real` `Real.instLE` `Norm.norm` `hasOpNorm` `NNReal.toReal`	—	`opNorm_le_bound` `map_zero` `AddMonoidHomClass.toZeroHomClass` `toAddMonoidHomClass` `dist_zero_right` `LipschitzWith.dist_le_mul`
`opNorm_neg` 📖	mathematical	—	`Norm.norm` `NormedAddGroupHom` `hasOpNorm` `neg`	—	`norm_neg`
`opNorm_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `NormedAddGroupHom` `hasOpNorm`	—	`le_csInf` `bounds_nonempty`
`opNorm_zero` 📖	mathematical	—	`Norm.norm` `NormedAddGroupHom` `hasOpNorm` `zero` `Real` `Real.instZero`	—	`le_antisymm` `csInf_le` `bounds_bddBelow` `ge_of_eq` `le_of_eq` `MulZeroClass.zero_mul` `norm_zero` `opNorm_nonneg`
`opNorm_zero_iff` 📖	mathematical	—	`Norm.norm` `NormedAddGroupHom` `NormedAddCommGroup.toSeminormedAddCommGroup` `hasOpNorm` `Real` `Real.instZero` `zero`	—	`ext` `norm_le_zero_iff` `le_opNorm` `MulZeroClass.zero_mul` `opNorm_zero`
`range_comp_incl_top` 📖	mathematical	—	`range` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Top.top` `AddSubgroup.instTop` `AddSubgroup.seminormedAddCommGroup` `comp` `incl`	—	`comp_range` `incl_range`
`ratio_le_opNorm` 📖	mathematical	—	`Real` `Real.instLE` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `NormedAddGroupHom` `funLike` `hasOpNorm`	—	`div_le_of_le_mul₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg` `opNorm_nonneg` `le_opNorm`
`smulCommClass` 📖	mathematical	—	`SMulCommClass` `NormedAddGroupHom` `smul`	—	`ext` `SMulCommClass.smul_comm`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	—
`sum_apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `Finset.sum` `AddCommGroup.toAddCommMonoid` `toAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup`	—	`coe_sum` `Finset.sum_apply`
`toAddMonoidHomClass` 📖	mathematical	—	`AddMonoidHomClass` `NormedAddGroupHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `funLike`	—	`map_add'` `AddMonoidHom.map_zero`
`toAddMonoidHom_injective` 📖	mathematical	—	`NormedAddGroupHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `toAddMonoidHom`	—	`coe_toAddMonoidHom`
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `NormedAddGroupHom` `funLike`	—	—
`uniformContinuous` 📖	mathematical	—	`UniformContinuous` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `NormedAddGroupHom` `funLike`	—	`LipschitzWith.uniformContinuous` `opNorm_nonneg` `lipschitz`
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`zero_comp` 📖	mathematical	—	`comp` `NormedAddGroupHom` `zero`	—	`ext`
`zsmul_apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `funLike` `zsmul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	—

NormedAddGroupHom.Equalizer

Definitions

Name	Category	Theorems
`liftEquiv` 📖	CompOp	2 math math: `liftEquiv_apply`, `liftEquiv_symm_apply_coe`
`map` 📖	CompOp	5 math math: `map_normNoninc`, `ι_comp_map`, `norm_map_le`, `map_comp_map`, `map_id`
`ι` 📖	CompOp	5 math math: `ι_normNoninc`, `ι_comp_map`, `ι_comp_lift`, `comp_ι_eq`, `liftEquiv_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm_sq₂` 📖	—	`NormedAddGroupHom.comp`	—	—	`NormedAddGroupHom.comp_assoc`
`comp_ι_eq` 📖	mathematical	—	`NormedAddGroupHom.comp` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup` `ι`	—	`NormedAddGroupHom.ext` `NormedAddGroupHom.comp_apply` `sub_eq_zero` `NormedAddGroupHom.sub_apply`
`liftEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `NormedAddGroupHom` `NormedAddGroupHom.comp` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftEquiv` `lift`	—	—
`liftEquiv_symm_apply_coe` 📖	mathematical	—	`NormedAddGroupHom` `NormedAddGroupHom.comp` `DFunLike.coe` `Equiv` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `liftEquiv` `ι`	—	—
`lift_apply_coe` 📖	mathematical	`NormedAddGroupHom.comp`	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `DFunLike.coe` `NormedAddGroupHom` `AddSubgroup.seminormedAddCommGroup` `NormedAddGroupHom.funLike` `lift`	—	—
`lift_normNoninc` 📖	mathematical	`NormedAddGroupHom.comp` `NormedAddGroupHom.NormNoninc`	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup` `lift`	—	—
`map_comp_map` 📖	mathematical	`NormedAddGroupHom.comp`	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup` `map` `comm_sq₂`	—	`NormedAddGroupHom.ext` `comm_sq₂`
`map_id` 📖	mathematical	—	`map` `NormedAddGroupHom.id` `NormedAddGroupHom` `NormedAddGroupHom.comp` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup`	—	`NormedAddGroupHom.ext`
`map_normNoninc` 📖	mathematical	`NormedAddGroupHom.comp` `NormedAddGroupHom.NormNoninc`	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup` `map`	—	`lift_normNoninc` `NormedAddGroupHom.NormNoninc.comp` `ι_normNoninc`
`norm_lift_le` 📖	mathematical	`NormedAddGroupHom.comp` `Real` `Real.instLE` `Norm.norm` `NormedAddGroupHom` `NormedAddGroupHom.hasOpNorm`	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup` `lift`	—	—
`norm_map_le` 📖	mathematical	`NormedAddGroupHom.comp` `Real` `Real.instLE` `Norm.norm` `NormedAddGroupHom` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup` `NormedAddGroupHom.hasOpNorm` `ι`	`map`	—	`norm_lift_le`
`ι_comp_lift` 📖	mathematical	`NormedAddGroupHom.comp`	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup` `ι` `lift`	—	`NormedAddGroupHom.ext`
`ι_comp_map` 📖	mathematical	`NormedAddGroupHom.comp`	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup` `ι` `map`	—	`ι_comp_lift`
`ι_normNoninc` 📖	mathematical	—	`NormedAddGroupHom.NormNoninc` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.equalizer` `AddSubgroup.seminormedAddCommGroup` `ι`	—	`le_rfl`

NormedAddGroupHom.NormNoninc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`NormedAddGroupHom.NormNoninc`	`NormedAddGroupHom.comp`	—	`LE.le.trans`
`id` 📖	mathematical	—	`NormedAddGroupHom.NormNoninc` `NormedAddGroupHom.id`	—	`le_rfl`
`neg_iff` 📖	mathematical	—	`NormedAddGroupHom.NormNoninc` `NormedAddGroupHom` `NormedAddGroupHom.neg`	—	`norm_neg` `LE.le.trans` `Eq.le`
`normNoninc_iff_norm_le_one` 📖	mathematical	—	`NormedAddGroupHom.NormNoninc` `Real` `Real.instLE` `Norm.norm` `NormedAddGroupHom` `NormedAddGroupHom.hasOpNorm` `Real.instOne`	—	`NormedAddGroupHom.opNorm_le_bound` `zero_le_one` `Real.instZeroLEOneClass` `one_mul` `NormedAddGroupHom.le_of_opNorm_le`
`zero` 📖	mathematical	—	`NormedAddGroupHom.NormNoninc` `NormedAddGroupHom` `NormedAddGroupHom.zero`	—	`norm_zero`

NormedAddGroupHom.SurjectiveOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_pos` 📖	mathematical	`NormedAddGroupHom.SurjectiveOnWith`	`Real` `Real.instLT` `Real.instZero`	—	`lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `mono` `le_of_not_gt` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `le_abs_self`
`mono` 📖	—	`NormedAddGroupHom.SurjectiveOnWith` `Real` `Real.instLE`	—	—	`MulZeroClass.mul_zero` `LE.le.trans` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `le_of_lt` `lt_of_le_of_ne'` `norm_nonneg`
`surjOn` 📖	mathematical	`NormedAddGroupHom.SurjectiveOnWith`	`Set.SurjOn` `DFunLike.coe` `NormedAddGroupHom` `NormedAddGroupHom.funLike` `Set.univ` `SetLike.coe` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddSubgroup.instSetLike`	—	`Set.mem_univ`

NormedAddGroupHom.ker

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`incl_comp_lift` 📖	mathematical	`NormedAddGroupHom.comp` `NormedAddGroupHom` `NormedAddGroupHom.zero`	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.ker` `AddSubgroup.seminormedAddCommGroup` `NormedAddGroupHom.incl` `lift`	—	`NormedAddGroupHom.ext`
`lift_apply_coe` 📖	mathematical	`NormedAddGroupHom.comp` `NormedAddGroupHom` `NormedAddGroupHom.zero`	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `NormedAddGroupHom.ker` `DFunLike.coe` `AddSubgroup.seminormedAddCommGroup` `NormedAddGroupHom.funLike` `lift`	—	—

(root)

Definitions

Name	Category	Theorems
`NormedAddGroupHom` 📖	CompData	141 math math: `SemiNormedGrp₁.hom_mkHom`, `SemiNormedGrp₁.comp_apply`, `NormedAddGroupHom.norm_id_of_nontrivial_seminorm`, `NormedAddGroupHom.completion_def`, `NormedAddGroupHom.norm_comp_le`, `AddSubgroup.norm_normedMk_le`, `NormedAddGroupHom.coe_toAddMonoidHom`, `SemiNormedGrp₁.coe_id`, `NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one`, `NormedAddGroupHom.norm_id_le`, `SemiNormedGrp.explicitCokernelπ_desc_apply`, `SemiNormedGrp.hom_sub`, `SemiNormedGrp₁.mkHom_hom`, `NormedAddCommGroup.norm_toCompl`, `NormedAddGroupHom.zero_completion`, `NormedAddGroupHom.coe_mkNormedAddGroupHom'`, `SemiNormedGrp₁.hom_comp`, `NormedAddGroupHom.instContinuousMapClass`, `NormedAddGroupHom.NormNoninc.zero`, `NormedAddGroupHom.smulCommClass`, `SemiNormedGrp.coe_comp`, `NormedAddGroupHom.smul_apply`, `NormedAddGroupHom.add_apply`, `NormedAddGroupHom.toFun_eq_coe`, `NormedAddGroupHom.extension_coe_to_fun`, `SeparationQuotient.liftNormedAddGroupHomEquiv_apply`, `NormedAddGroupHom.IsQuotient.norm_le`, `NormedAddGroupHom.neg_apply`, `AddSubgroup.norm_trivial_quotient_mk`, `NormedAddGroupHom.isCentralScalar`, `SemiNormedGrp.ext_iff`, `SemiNormedGrp₁.hom_id`, `NormedAddGroupHom.norm_completion`, `SeparationQuotient.norm_normedMk_eq_one`, `SeparationQuotient.norm_normedMk_le`, `NormedAddGroupHom.mkNormedAddGroupHom_norm_le`, `NormedAddGroupHom.completion_sub`, `SemiNormedGrp.zero_apply`, `NormedAddGroupHom.coe_mkNormedAddGroupHom`, `NormedAddGroupHom.completion_coe`, `NormedAddGroupHom.isometry_id`, `NormedAddCommGroup.denseRange_toCompl`, `SemiNormedGrp.id_apply`, `NormedAddGroupHom.mem_ker`, `NormedAddGroupHom.coe_comp`, `NormedAddGroupHom.le_opNorm_of_le`, `SemiNormedGrp.completion.norm_incl_eq`, `NormedAddGroupHom.coe_nsmul`, `NormedAddGroupHom.extension_coe`, `NormedAddGroupHom.zero_apply`, `SemiNormedGrp.hom_add`, `NormedAddGroupHom.completion_add`, `NormedAddGroupHom.mkNormedAddGroupHom_norm_le'`, `normedAddGroupHomCompletionHom_apply`, `NormedAddGroupHom.uniformContinuous`, `NormedAddGroupHom.IsQuotient.norm_lift`, `NormedAddGroupHom.sub_apply`, `SemiNormedGrp.hom_neg`, `SeparationQuotient.normedMk_eq_zero_iff`, `NormedAddGroupHom.Equalizer.liftEquiv_apply`, `NormedAddGroupHom.opNorm_add_le`, `NormedAddGroupHom.ratio_le_opNorm`, `SemiNormedGrp.inv_hom_apply`, `NormedAddGroupHom.completion_coe_to_fun`, `SemiNormedGrp₁.iso_isometry`, `NormedAddGroupHom.opNorm_zero_iff`, `SemiNormedGrp₁.mkHom_apply`, `NormedAddGroupHom.toAddMonoidHom_injective`, `NormedAddGroupHom.coe_neg`, `SemiNormedGrp.explicitCokernelπ_apply_dom_eq_zero`, `SemiNormedGrp₁.coe_comp`, `SemiNormedGrp.explicitCokernelπ_surjective`, `NormedAddGroupHom.bound`, `NormedAddGroupHom.incl_apply`, `NormedAddGroupHom.id_apply`, `NormedAddGroupHom.coe_sum`, `NormedAddGroupHom.le_opNorm`, `NormedAddGroupHom.comp_apply`, `NormedAddGroupHom.SurjectiveOnWith.surjOn`, `NormedAddGroupHom.Equalizer.lift_apply_coe`, `SemiNormedGrp₁.ext_iff`, `NormedAddGroupHom.ofLipschitz_norm_le`, `AddSubgroup.surjective_normedMk`, `AddMonoidHom.mkNormedAddGroupHom_norm_le`, `NormedAddGroupHom.coe_sub`, `SemiNormedGrp.ofHom_apply`, `NormedAddGroupHom.opNorm_neg`, `SemiNormedGrp₁.instAddMonoidHomClassSubtypeNormedAddGroupHomCarrierNormNoninc`, `NormedAddGroupHom.completion_neg`, `NormedAddGroupHom.IsQuotient.norm`, `NormedAddGroupHom.opNorm_nonneg`, `SemiNormedGrp₁.zero_apply`, `NormedAddGroupHom.coe_ker`, `SemiNormedGrp₁.id_apply`, `NormedAddGroupHom.toAddMonoidHomClass`, `NormedAddGroupHom.mem_range_self`, `SeparationQuotient.normedMk_apply`, `SemiNormedGrp.coe_id`, `NormedAddCommGroup.toCompl_apply`, `NormedAddGroupHom.coe_injective`, `SemiNormedGrp₁.hom_inv_apply`, `SemiNormedGrp.hom_zero`, `NormedAddGroupHom.isScalarTower`, `NormedAddGroupHom.lipschitz`, `NormedAddGroupHom.coe_id`, `NormedAddGroupHom.nsmul_apply`, `NormedAddGroupHom.coeAddHom_apply`, `NormedAddGroupHom.Equalizer.map_id`, `NormedAddGroupHom.zero_comp`, `NormedAddGroupHom.extension_def`, `NormedAddGroupHom.NormNoninc.neg_iff`, `SemiNormedGrp.comp_apply`, `NormedAddGroupHom.completion_coe'`, `NormedAddGroupHom.coe_mk`, `NormedAddGroupHom.mem_range`, `AddSubgroup.norm_normedMk`, `AddMonoidHom.mkNormedAddGroupHom_norm_le'`, `NormedAddGroupHom.coe_add`, `NormedAddGroupHom.sum_apply`, `NormedAddGroupHom.norm_def`, `NormedAddGroupHom.opNorm_zero`, `NormedAddGroupHom.IsQuotient.surjective`, `NormedAddGroupHom.coe_smul`, `NormedAddGroupHom.coe_inj_iff`, `SemiNormedGrp.iso_isometry_of_normNoninc`, `AddSubgroup.normedMk.apply`, `NormedAddGroupHom.ker_zero`, `NormedAddGroupHom.coe_zero`, `NormedAddGroupHom.ext_iff`, `SeparationQuotient.liftNormedAddGroupHomEquiv_symm_apply_coe`, `NormedAddGroupHom.comp_zero`, `NormedAddGroupHom.zsmul_apply`, `SemiNormedGrp.hom_inv_apply`, `SemiNormedGrp.hom_zsum`, `SemiNormedGrp₁.inv_hom_apply`, `NormedAddGroupHom.Equalizer.liftEquiv_symm_apply_coe`, `NormedAddGroupHom.continuous`, `SemiNormedGrp.hom_nsum`, `NormedAddGroupHom.norm_incl`, `NormedAddGroupHom.norm_id`, `NormedAddGroupHom.coe_zsmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_pos_bound_of_bound` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul`	`Real.instLT` `Real.instZero`	—	`lt_of_lt_of_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `le_max_right` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `le_max_left` `norm_nonneg`

---

← Back to Index