SemiNormedGrp

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

Statistics

Metric	Count
Definitions SemiNormedGrp, hom, add, addCommGroup, hom, hom', neg, nsmul, sub, zsmul, carrier, instCoeSortType, instConcreteCategoryNormedAddGroupHomCarrier, instHasZeroMorphisms, instInhabited, instLargeCategory, instZeroHom, ofHom, str, SemiNormedGrp₁, hom, hom, hom', carrier, instCoeFunHomForallCarrier, instCoeSortType, instConcreteCategorySubtypeNormedAddGroupHomCarrierNormNoninc, instFunLike, instHasForget₂SubtypeNormedAddGroupHomCarrierNormNonincSemiNormedGrpCarrier, instHasZeroMorphisms, instInhabited, instLargeCategory, instSeminormedAddCommGroupCarrier, instZeroHom, mkHom, mkIso, str	37
Theorems ext, ext_iff, coe_comp, coe_id, coe_of, comp_apply, ext, ext_iff, hasZeroObject, hom_add, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_neg, hom_nsum, hom_ofHom, hom_sub, hom_zero, hom_zsum, id_apply, inv_hom_apply, isZero_of_subsingleton, iso_isometry_of_normNoninc, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, zero_apply, ext, ext_iff, normNoninc, coe_comp, coe_id, coe_of, comp_apply, ext, ext_iff, hasZeroObject, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_mkHom, id_apply, instAddMonoidHomClassSubtypeNormedAddGroupHomCarrierNormNoninc, inv_hom_apply, isZero_of_subsingleton, iso_isometry, mkHom_apply, mkHom_comp, mkHom_hom, mkHom_id, mkIso_hom, mkIso_inv, zero_apply	58
Total	95

SemiNormedGrp

Definitions

Name	Category	Theorems
carrier 📖	CompOp	29 math math: explicitCokernelπ_desc_apply, hom_sub, hom_id, coe_comp, ext_iff, isQuotient_explicitCokernelπ, zero_apply, id_apply, completion.norm_incl_eq, hom_add, hom_neg, inv_hom_apply, explicitCokernelπ_apply_dom_eq_zero, explicitCokernelπ_surjective, hom_comp, completion_obj_str, ofHom_apply, normNoninc_explicitCokernelπ, coe_id, hom_zero, comp_apply, ofHom_hom, completion_map, hom_inv_apply, hom_zsum, completion_obj_carrier, coe_of, hom_nsum, completion_completeSpace
instCoeSortType 📖	CompOp	—
instConcreteCategoryNormedAddGroupHomCarrier 📖	CompOp	14 math math: explicitCokernelπ_desc_apply, coe_comp, ext_iff, zero_apply, id_apply, completion.norm_incl_eq, inv_hom_apply, explicitCokernelπ_apply_dom_eq_zero, explicitCokernelπ_surjective, ofHom_apply, coe_id, comp_apply, iso_isometry_of_normNoninc, hom_inv_apply
instHasZeroMorphisms 📖	CompOp	4 math math: explicitCokernelIso_hom_π, explicitCokernelIso_hom_desc, explicitCokernelIso_inv_π, instHasCokernels
instInhabited 📖	CompOp	—
instLargeCategory 📖	CompOp	42 math math: hom_sub, hom_id, coe_comp, ext_iff, explicitCokernelπ.epi, zero_apply, isZero_of_subsingleton, id_apply, completion.norm_incl_eq, hom_add, instHasEqualizers, instAdditiveCompletion, hom_neg, explicitCokernel_hom_ext_iff, inv_hom_apply, completion.map_normNoninc, explicitCokernelπ_apply_dom_eq_zero, explicitCokernelπ_surjective, hom_comp, hasLimit_parallelPair, explicitCokernelIso_hom_π, completion_obj_str, completion.lift_comp_incl, completion.map_zero, ofHom_apply, hasZeroObject, explicitCokernelDesc_zero, comp_explicitCokernelπ, coe_id, hom_zero, ofHom_id, comp_apply, comp_explicitCokernelπ_assoc, explicitCokernelIso_inv_π, ofHom_comp, instHasCokernels, completion_map, hom_inv_apply, hom_zsum, completion_obj_carrier, hom_nsum, completion_completeSpace
instZeroHom 📖	CompOp	6 math math: zero_apply, completion.map_zero, explicitCokernelDesc_zero, comp_explicitCokernelπ, hom_zero, comp_explicitCokernelπ_assoc
ofHom 📖	CompOp	6 math math: hom_ofHom, ofHom_apply, ofHom_id, ofHom_hom, ofHom_comp, completion_map
str 📖	CompOp	28 math math: explicitCokernelπ_desc_apply, hom_sub, hom_id, coe_comp, ext_iff, isQuotient_explicitCokernelπ, zero_apply, id_apply, completion.norm_incl_eq, hom_add, hom_neg, inv_hom_apply, explicitCokernelπ_apply_dom_eq_zero, explicitCokernelπ_surjective, hom_comp, completion_obj_str, ofHom_apply, normNoninc_explicitCokernelπ, coe_id, hom_zero, comp_apply, ofHom_hom, completion_map, hom_inv_apply, hom_zsum, completion_obj_carrier, hom_nsum, completion_completeSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemiNormedGrp instLargeCategory NormedAddGroupHom str NormedAddGroupHom.funLike instConcreteCategoryNormedAddGroupHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemiNormedGrp instLargeCategory NormedAddGroupHom str NormedAddGroupHom.funLike instConcreteCategoryNormedAddGroupHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemiNormedGrp instLargeCategory NormedAddGroupHom str NormedAddGroupHom.funLike instConcreteCategoryNormedAddGroupHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
ext 📖	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemiNormedGrp instLargeCategory NormedAddGroupHom str NormedAddGroupHom.funLike instConcreteCategoryNormedAddGroupHomCarrier	—	—	CategoryTheory.ConcreteCategory.ext_apply
ext_iff 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemiNormedGrp instLargeCategory NormedAddGroupHom str NormedAddGroupHom.funLike instConcreteCategoryNormedAddGroupHomCarrier	—	ext
hasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject SemiNormedGrp instLargeCategory	—	isZero_of_subsingleton
hom_add 📖	mathematical	—	Hom.hom Quiver.Hom SemiNormedGrp CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instLargeCategory Hom.add NormedAddGroupHom carrier str NormedAddGroupHom.add	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp SemiNormedGrp CategoryTheory.Category.toCategoryStruct instLargeCategory NormedAddGroupHom.comp carrier str	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id SemiNormedGrp CategoryTheory.Category.toCategoryStruct instLargeCategory NormedAddGroupHom.id carrier str	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemiNormedGrp instLargeCategory NormedAddGroupHom str NormedAddGroupHom.funLike instConcreteCategoryNormedAddGroupHomCarrier CategoryTheory.Iso.hom CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id_apply
hom_neg 📖	mathematical	—	Hom.hom Quiver.Hom SemiNormedGrp CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instLargeCategory Hom.neg NormedAddGroupHom carrier str NormedAddGroupHom.neg	—	—
hom_nsum 📖	mathematical	—	Hom.hom Quiver.Hom SemiNormedGrp CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instLargeCategory Hom.nsmul NormedAddGroupHom carrier str NormedAddGroupHom.nsmul	—	—
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—
hom_sub 📖	mathematical	—	Hom.hom Quiver.Hom SemiNormedGrp CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instLargeCategory Hom.sub NormedAddGroupHom carrier str NormedAddGroupHom.sub	—	—
hom_zero 📖	mathematical	—	Hom.hom Quiver.Hom SemiNormedGrp CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instLargeCategory instZeroHom NormedAddGroupHom carrier str NormedAddGroupHom.zero	—	—
hom_zsum 📖	mathematical	—	Hom.hom Quiver.Hom SemiNormedGrp CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instLargeCategory Hom.zsmul NormedAddGroupHom carrier str NormedAddGroupHom.zsmul	—	—
id_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemiNormedGrp instLargeCategory NormedAddGroupHom str NormedAddGroupHom.funLike instConcreteCategoryNormedAddGroupHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemiNormedGrp instLargeCategory NormedAddGroupHom str NormedAddGroupHom.funLike instConcreteCategoryNormedAddGroupHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
isZero_of_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero SemiNormedGrp instLargeCategory	—	hom_ext NormedAddGroupHom.ext map_zero AddMonoidHomClass.toZeroHomClass NormedAddGroupHom.toAddMonoidHomClass
iso_isometry_of_normNoninc 📖	mathematical	NormedAddGroupHom.NormNoninc carrier str Hom.hom CategoryTheory.Iso.hom SemiNormedGrp instLargeCategory CategoryTheory.Iso.inv	Isometry PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom NormedAddGroupHom NormedAddGroupHom.funLike instConcreteCategoryNormedAddGroupHomCarrier	—	AddMonoidHomClass.isometry_of_norm NormedAddGroupHom.toAddMonoidHomClass le_antisymm comp_apply CategoryTheory.Iso.hom_inv_id id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom SemiNormedGrp instLargeCategory NormedAddGroupHom str NormedAddGroupHom.funLike instConcreteCategoryNormedAddGroupHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom NormedAddGroupHom.comp CategoryTheory.CategoryStruct.comp SemiNormedGrp CategoryTheory.Category.toCategoryStruct instLargeCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier str Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom NormedAddGroupHom.id CategoryTheory.CategoryStruct.id SemiNormedGrp CategoryTheory.Category.toCategoryStruct instLargeCategory of	—	—
zero_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemiNormedGrp instLargeCategory NormedAddGroupHom str NormedAddGroupHom.funLike instConcreteCategoryNormedAddGroupHomCarrier Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instZeroHom NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—

SemiNormedGrp.Hom

Definitions

Name	Category	Theorems
add 📖	CompOp	1 math math: SemiNormedGrp.hom_add
addCommGroup 📖	CompOp	—
hom 📖	CompOp	14 math math: SemiNormedGrp.hom_sub, SemiNormedGrp.hom_id, SemiNormedGrp.hom_ext_iff, SemiNormedGrp.isQuotient_explicitCokernelπ, SemiNormedGrp.hom_add, SemiNormedGrp.hom_ofHom, SemiNormedGrp.hom_neg, SemiNormedGrp.hom_comp, SemiNormedGrp.normNoninc_explicitCokernelπ, SemiNormedGrp.hom_zero, SemiNormedGrp.ofHom_hom, SemiNormedGrp.completion_map, SemiNormedGrp.hom_zsum, SemiNormedGrp.hom_nsum
hom' 📖	CompOp	1 math math: ext_iff
neg 📖	CompOp	1 math math: SemiNormedGrp.hom_neg
nsmul 📖	CompOp	1 math math: SemiNormedGrp.hom_nsum
sub 📖	CompOp	1 math math: SemiNormedGrp.hom_sub
zsmul 📖	CompOp	1 math math: SemiNormedGrp.hom_zsum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom'	—	—	—
ext_iff 📖	mathematical	—	hom'	—	ext

SemiNormedGrp.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

SemiNormedGrp₁

Definitions

Name	Category	Theorems
carrier 📖	CompOp	17 math math: hom_mkHom, comp_apply, coe_id, mkHom_hom, hom_comp, hom_id, Hom.normNoninc, iso_isometry, mkHom_apply, coe_of, coe_comp, ext_iff, instAddMonoidHomClassSubtypeNormedAddGroupHomCarrierNormNoninc, zero_apply, id_apply, hom_inv_apply, inv_hom_apply
instCoeFunHomForallCarrier 📖	CompOp	—
instCoeSortType 📖	CompOp	—
instConcreteCategorySubtypeNormedAddGroupHomCarrierNormNoninc 📖	CompOp	—
instFunLike 📖	CompOp	1 math math: instAddMonoidHomClassSubtypeNormedAddGroupHomCarrierNormNoninc
instHasForget₂SubtypeNormedAddGroupHomCarrierNormNonincSemiNormedGrpCarrier 📖	CompOp	—
instHasZeroMorphisms 📖	CompOp	1 math math: instHasCokernels
instInhabited 📖	CompOp	—
instLargeCategory 📖	CompOp	17 math math: comp_apply, coe_id, hom_comp, hom_id, iso_isometry, coe_comp, mkHom_comp, zero_apply, id_apply, mkHom_id, mkIso_inv, hom_inv_apply, hasZeroObject, isZero_of_subsingleton, inv_hom_apply, mkIso_hom, instHasCokernels
instSeminormedAddCommGroupCarrier 📖	CompOp	2 math math: iso_isometry, zero_apply
instZeroHom 📖	CompOp	1 math math: zero_apply
mkHom 📖	CompOp	7 math math: hom_mkHom, mkHom_hom, mkHom_apply, mkHom_comp, mkHom_id, mkIso_inv, mkIso_hom
mkIso 📖	CompOp	2 math math: mkIso_inv, mkIso_hom
str 📖	CompOp	16 math math: hom_mkHom, comp_apply, coe_id, mkHom_hom, hom_comp, hom_id, Hom.normNoninc, iso_isometry, mkHom_apply, coe_comp, ext_iff, instAddMonoidHomClassSubtypeNormedAddGroupHomCarrierNormNoninc, zero_apply, id_apply, hom_inv_apply, inv_hom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe NormedAddGroupHom carrier str NormedAddGroupHom.funLike NormedAddGroupHom.NormNoninc Hom.hom CategoryTheory.CategoryStruct.comp SemiNormedGrp₁ CategoryTheory.Category.toCategoryStruct instLargeCategory	—	—
coe_id 📖	mathematical	—	DFunLike.coe NormedAddGroupHom carrier str NormedAddGroupHom.funLike NormedAddGroupHom.NormNoninc Hom.hom CategoryTheory.CategoryStruct.id SemiNormedGrp₁ CategoryTheory.Category.toCategoryStruct instLargeCategory	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe NormedAddGroupHom carrier str NormedAddGroupHom.funLike NormedAddGroupHom.NormNoninc Hom.hom CategoryTheory.CategoryStruct.comp SemiNormedGrp₁ CategoryTheory.Category.toCategoryStruct instLargeCategory	—	—
ext 📖	—	DFunLike.coe NormedAddGroupHom carrier str NormedAddGroupHom.funLike NormedAddGroupHom.NormNoninc Hom.hom	—	—	CategoryTheory.ConcreteCategory.ext_apply
ext_iff 📖	mathematical	—	DFunLike.coe NormedAddGroupHom carrier str NormedAddGroupHom.funLike NormedAddGroupHom.NormNoninc Hom.hom	—	ext
hasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject SemiNormedGrp₁ instLargeCategory	—	isZero_of_subsingleton
hom_comp 📖	mathematical	—	NormedAddGroupHom carrier str NormedAddGroupHom.NormNoninc Hom.hom CategoryTheory.CategoryStruct.comp SemiNormedGrp₁ CategoryTheory.Category.toCategoryStruct instLargeCategory NormedAddGroupHom.comp	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	NormedAddGroupHom carrier str NormedAddGroupHom.NormNoninc Hom.hom CategoryTheory.CategoryStruct.id SemiNormedGrp₁ CategoryTheory.Category.toCategoryStruct instLargeCategory NormedAddGroupHom.id	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe NormedAddGroupHom carrier str NormedAddGroupHom.funLike NormedAddGroupHom.NormNoninc Hom.hom CategoryTheory.Iso.hom SemiNormedGrp₁ instLargeCategory CategoryTheory.Iso.inv	—	comp_apply CategoryTheory.Iso.inv_hom_id
hom_mkHom 📖	mathematical	NormedAddGroupHom.NormNoninc	NormedAddGroupHom carrier of str Hom.hom mkHom	—	—
id_apply 📖	mathematical	—	DFunLike.coe NormedAddGroupHom carrier str NormedAddGroupHom.funLike NormedAddGroupHom.NormNoninc Hom.hom CategoryTheory.CategoryStruct.id SemiNormedGrp₁ CategoryTheory.Category.toCategoryStruct instLargeCategory	—	—
instAddMonoidHomClassSubtypeNormedAddGroupHomCarrierNormNoninc 📖	mathematical	—	AddMonoidHomClass NormedAddGroupHom carrier str NormedAddGroupHom.NormNoninc AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instFunLike	—	map_add AddMonoidHomClass.toAddHomClass NormedAddGroupHom.toAddMonoidHomClass map_zero AddMonoidHomClass.toZeroHomClass
inv_hom_apply 📖	mathematical	—	DFunLike.coe NormedAddGroupHom carrier str NormedAddGroupHom.funLike NormedAddGroupHom.NormNoninc Hom.hom CategoryTheory.Iso.inv SemiNormedGrp₁ instLargeCategory CategoryTheory.Iso.hom	—	comp_apply CategoryTheory.Iso.hom_inv_id
isZero_of_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero SemiNormedGrp₁ instLargeCategory	—	hom_ext NormedAddGroupHom.ext map_zero AddMonoidHomClass.toZeroHomClass NormedAddGroupHom.toAddMonoidHomClass
iso_isometry 📖	mathematical	—	Isometry carrier PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace instSeminormedAddCommGroupCarrier DFunLike.coe NormedAddGroupHom str NormedAddGroupHom.funLike NormedAddGroupHom.NormNoninc Hom.hom CategoryTheory.Iso.hom SemiNormedGrp₁ instLargeCategory	—	AddMonoidHomClass.isometry_of_norm AddMonoidHom.instAddMonoidHomClass map_zero AddMonoidHomClass.toZeroHomClass NormedAddGroupHom.toAddMonoidHomClass map_add AddMonoidHomClass.toAddHomClass le_antisymm Hom.normNoninc comp_apply CategoryTheory.Iso.hom_inv_id id_apply
mkHom_apply 📖	mathematical	NormedAddGroupHom.NormNoninc	DFunLike.coe NormedAddGroupHom carrier of str NormedAddGroupHom.funLike Hom.hom mkHom	—	—
mkHom_comp 📖	mathematical	NormedAddGroupHom.NormNoninc NormedAddGroupHom.comp	mkHom CategoryTheory.CategoryStruct.comp SemiNormedGrp₁ CategoryTheory.Category.toCategoryStruct instLargeCategory of	—	—
mkHom_hom 📖	mathematical	—	mkHom carrier str NormedAddGroupHom NormedAddGroupHom.NormNoninc Hom.hom Hom.normNoninc	—	Hom.normNoninc
mkHom_id 📖	mathematical	—	mkHom NormedAddGroupHom.id NormedAddGroupHom.NormNoninc.id CategoryTheory.CategoryStruct.id SemiNormedGrp₁ CategoryTheory.Category.toCategoryStruct instLargeCategory of	—	NormedAddGroupHom.NormNoninc.id
mkIso_hom 📖	mathematical	NormedAddGroupHom.NormNoninc SemiNormedGrp.carrier SemiNormedGrp.str SemiNormedGrp.Hom.hom CategoryTheory.Iso.hom SemiNormedGrp SemiNormedGrp.instLargeCategory CategoryTheory.Iso.inv	SemiNormedGrp₁ instLargeCategory of mkIso mkHom	—	—
mkIso_inv 📖	mathematical	NormedAddGroupHom.NormNoninc SemiNormedGrp.carrier SemiNormedGrp.str SemiNormedGrp.Hom.hom CategoryTheory.Iso.hom SemiNormedGrp SemiNormedGrp.instLargeCategory CategoryTheory.Iso.inv	SemiNormedGrp₁ instLargeCategory of mkIso mkHom	—	—
zero_apply 📖	mathematical	—	DFunLike.coe NormedAddGroupHom carrier str NormedAddGroupHom.funLike NormedAddGroupHom.NormNoninc Hom.hom Quiver.Hom SemiNormedGrp₁ CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instLargeCategory instZeroHom NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instSeminormedAddCommGroupCarrier	—	—

SemiNormedGrp₁.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	15 math math: SemiNormedGrp₁.hom_mkHom, SemiNormedGrp₁.comp_apply, SemiNormedGrp₁.coe_id, SemiNormedGrp₁.mkHom_hom, SemiNormedGrp₁.hom_comp, SemiNormedGrp₁.hom_id, SemiNormedGrp₁.hom_ext_iff, SemiNormedGrp₁.iso_isometry, SemiNormedGrp₁.mkHom_apply, SemiNormedGrp₁.coe_comp, SemiNormedGrp₁.ext_iff, SemiNormedGrp₁.zero_apply, SemiNormedGrp₁.id_apply, SemiNormedGrp₁.hom_inv_apply, SemiNormedGrp₁.inv_hom_apply
hom' 📖	CompOp	2 math math: normNoninc, ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom'	—	—	—
ext_iff 📖	mathematical	—	hom'	—	ext
normNoninc 📖	mathematical	—	NormedAddGroupHom.NormNoninc SemiNormedGrp₁.carrier SemiNormedGrp₁.str hom'	—	—

SemiNormedGrp₁.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
SemiNormedGrp 📖	CompData	42 math math: SemiNormedGrp.hom_sub, SemiNormedGrp.hom_id, SemiNormedGrp.coe_comp, SemiNormedGrp.ext_iff, SemiNormedGrp.explicitCokernelπ.epi, SemiNormedGrp.zero_apply, SemiNormedGrp.isZero_of_subsingleton, SemiNormedGrp.id_apply, SemiNormedGrp.completion.norm_incl_eq, SemiNormedGrp.hom_add, SemiNormedGrp.instHasEqualizers, SemiNormedGrp.instAdditiveCompletion, SemiNormedGrp.hom_neg, SemiNormedGrp.explicitCokernel_hom_ext_iff, SemiNormedGrp.inv_hom_apply, SemiNormedGrp.completion.map_normNoninc, SemiNormedGrp.explicitCokernelπ_apply_dom_eq_zero, SemiNormedGrp.explicitCokernelπ_surjective, SemiNormedGrp.hom_comp, SemiNormedGrp.hasLimit_parallelPair, SemiNormedGrp.explicitCokernelIso_hom_π, SemiNormedGrp.completion_obj_str, SemiNormedGrp.completion.lift_comp_incl, SemiNormedGrp.completion.map_zero, SemiNormedGrp.ofHom_apply, SemiNormedGrp.hasZeroObject, SemiNormedGrp.explicitCokernelDesc_zero, SemiNormedGrp.comp_explicitCokernelπ, SemiNormedGrp.coe_id, SemiNormedGrp.hom_zero, SemiNormedGrp.ofHom_id, SemiNormedGrp.comp_apply, SemiNormedGrp.comp_explicitCokernelπ_assoc, SemiNormedGrp.explicitCokernelIso_inv_π, SemiNormedGrp.ofHom_comp, SemiNormedGrp.instHasCokernels, SemiNormedGrp.completion_map, SemiNormedGrp.hom_inv_apply, SemiNormedGrp.hom_zsum, SemiNormedGrp.completion_obj_carrier, SemiNormedGrp.hom_nsum, SemiNormedGrp.completion_completeSpace
SemiNormedGrp₁ 📖	CompData	17 math math: SemiNormedGrp₁.comp_apply, SemiNormedGrp₁.coe_id, SemiNormedGrp₁.hom_comp, SemiNormedGrp₁.hom_id, SemiNormedGrp₁.iso_isometry, SemiNormedGrp₁.coe_comp, SemiNormedGrp₁.mkHom_comp, SemiNormedGrp₁.zero_apply, SemiNormedGrp₁.id_apply, SemiNormedGrp₁.mkHom_id, SemiNormedGrp₁.mkIso_inv, SemiNormedGrp₁.hom_inv_apply, SemiNormedGrp₁.hasZeroObject, SemiNormedGrp₁.isZero_of_subsingleton, SemiNormedGrp₁.inv_hom_apply, SemiNormedGrp₁.mkIso_hom, SemiNormedGrp₁.instHasCokernels

---

← Back to Index