| Metric | Count |
|---|
DefinitionsmkNormedAddGroupHom, 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 |
TheoremsmkNormedAddGroupHom_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_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 | 112 |
| Total | 146 |
| Name | Category | Theorems |
|---|
NormNoninc 📖 | MathDef | 30 mathmath: SemiNormedGrp₁.hom_mkHom, SemiNormedGrp₁.comp_apply, SeparationQuotient.liftNormedAddGroupHom_normNoninc, Equalizer.ι_normNoninc, SemiNormedGrp₁.coe_id, NormNoninc.normNoninc_iff_norm_le_one, SemiNormedGrp₁.mkHom_hom, SemiNormedGrp₁.hom_comp, NormNoninc.zero, Equalizer.map_normNoninc, SemiNormedGrp₁.hom_id, lift_normNoninc, SemiNormedGrp₁.Hom.normNoninc, NormNoninc.id, SemiNormedGrp.explicitCokernelDesc_normNoninc, SemiNormedGrp.completion.map_normNoninc, SemiNormedGrp₁.iso_isometry, SemiNormedGrp₁.mkHom_apply, Equalizer.lift_normNoninc, 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, NormNoninc.comp, SemiNormedGrp₁.inv_hom_apply
|
SurjectiveOnWith 📖 | MathDef | 4 mathmath: SurjectiveOnWith.mono, controlled_closure_of_complete, SurjectiveOnWith.exists_pos, controlled_closure_range_of_complete
|
add 📖 | CompOp | 5 mathmath: add_apply, SemiNormedGrp.hom_add, completion_add, opNorm_add_le, coe_add
|
coeAddHom 📖 | CompOp | 1 mathmath: coeAddHom_apply
|
comp 📖 | CompOp | 30 mathmath: norm_comp_le, SemiNormedGrp₁.hom_comp, comp_assoc, norm_comp_le_of_le, coe_comp, Equalizer.liftEquiv_apply, range_comp_incl_top, comp_range, Equalizer.ι_comp_map, SemiNormedGrp.hom_comp, Equalizer.ι_comp_lift, comp_apply, ker_completion, SemiNormedGrp₁.mkHom_comp, completion_toCompl, norm_comp_le_of_le', ker.incl_comp_lift, Equalizer.map_comp_map, Equalizer.comp_ι_eq, ker_le_ker_completion, completion_comp, Equalizer.map_id, Equalizer.comm_sq₂, 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 | 13 mathmath: Equalizer.ι_normNoninc, Equalizer.map_normNoninc, Equalizer.liftEquiv_apply, Equalizer.ι_comp_map, Equalizer.lift_normNoninc, Equalizer.norm_map_le, 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 | 95 mathmath: SemiNormedGrp₁.comp_apply, completion_def, coe_toAddMonoidHom, SemiNormedGrp₁.coe_id, SeparationQuotient.norm_liftNormedAddGroupHom_apply_le, SemiNormedGrp.explicitCokernelπ_desc_apply, NormedAddCommGroup.norm_toCompl, coe_mkNormedAddGroupHom', lift_mk, 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, norm_eq_of_isometry, 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, SeparationQuotient.liftNormedAddGroupHom_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, antilipschitz_of_norm_ge, zsmul_apply, SemiNormedGrp.hom_inv_apply, SemiNormedGrp₁.inv_hom_apply, continuous, isometry_comp, norm_incl, coe_zsmul
|
hasOpNorm 📖 | CompOp | 38 mathmath: 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, norm_comp_le_of_le, le_opNorm_of_le, mkNormedAddGroupHom_norm_le', opNorm_eq_of_bounds, opNorm_add_le, ratio_le_opNorm, opNorm_le_bound, opNorm_zero_iff, Equalizer.norm_map_le, SeparationQuotient.norm_liftNormedAddGroupHom_le, le_opNorm, QuotientAddGroup.norm_lift_apply_le, ofLipschitz_norm_le, AddMonoidHom.mkNormedAddGroupHom_norm_le, opNorm_neg, norm_comp_le_of_le', opNorm_nonneg, lift_norm_le, norm_lift_le, lipschitz, AddSubgroup.norm_normedMk, AddMonoidHom.mkNormedAddGroupHom_norm_le', Equalizer.norm_lift_le, norm_def, opNorm_zero, norm_id, SeparationQuotient.liftNormedAddGroupHom_norm_le
|
id 📖 | CompOp | 12 mathmath: 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 mathmath: 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 mathmath: 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 mathmath: neg_apply, SemiNormedGrp.hom_neg, coe_neg, opNorm_neg, completion_neg, NormNoninc.neg_iff
|
nsmul 📖 | CompOp | 3 mathmath: coe_nsmul, nsmul_apply, SemiNormedGrp.hom_nsum
|
ofLipschitz 📖 | CompOp | 1 mathmath: ofLipschitz_norm_le
|
opNorm 📖 | CompOp | — |
range 📖 | CompOp | 9 mathmath: incl_range, BoundedContinuousFunction.range_toLpHom, range_comp_incl_top, comp_range, ker_completion, controlled_closure_range_of_complete, mem_range_self, ker_le_ker_completion, mem_range
|
smul 📖 | CompOp | 5 mathmath: smulCommClass, smul_apply, isCentralScalar, isScalarTower, coe_smul
|
sub 📖 | CompOp | 4 mathmath: SemiNormedGrp.hom_sub, completion_sub, sub_apply, coe_sub
|
toAddCommGroup 📖 | CompOp | 2 mathmath: coe_sum, sum_apply
|
toAddMonoidHom 📖 | CompOp | 5 mathmath: coe_toAddMonoidHom, mk_toAddMonoidHom, comp_range, toAddMonoidHom_injective, QuotientAddGroup.norm_lift_apply_le
|
toFun 📖 | CompOp | 4 mathmath: toFun_eq_coe, map_add', bound', coe_injective
|
toNormedAddCommGroup 📖 | CompOp | 1 mathmath: normedAddGroupHomCompletionHom_apply
|
toSeminormedAddCommGroup 📖 | CompOp | 2 mathmath: normedAddGroupHomCompletionHom_apply, coeAddHom_apply
|
zero 📖 | CompOp | 11 mathmath: 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 mathmath: zsmul_apply, SemiNormedGrp.hom_zsum, coe_zsmul
|