Seminorm

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

Statistics

Metric	Count
Definitions `AddGroupNorm`, `funLike`, `instAdd`, `instInhabited`, `instMax`, `instOne`, `instPartialOrder`, `instSemilatticeSup`, `toAddGroupSeminorm`, `toOne`, `AddGroupSeminorm`, `comp`, `funLike`, `instAdd`, `instInhabited`, `instLattice`, `instMax`, `instMin`, `instPartialOrder`, `instSupSet`, `instZeroAddGroupSeminorm`, `semilatticeSup`, `toFun`, `toOne`, `toSMul`, `GroupNorm`, `funLike`, `instAdd`, `instInhabited`, `instMax`, `instPartialOrder`, `instSemilatticeSup`, `toGroupSeminorm`, `toOne`, `GroupSeminorm`, `comp`, `funLike`, `instAdd`, `instInhabited`, `instLattice`, `instMax`, `instMin`, `instPartialOrder`, `instSMul`, `instSupSet`, `instZeroGroupSeminorm`, `semilatticeSup`, `toFun`, `toOne`, `NonarchAddGroupNorm`, `funLike`, `instInhabitedOfDecidableEq`, `instMax`, `instOneOfDecidableEq`, `instPartialOrder`, `instSemilatticeSup`, `toNonarchAddGroupSeminorm`, `NonarchAddGroupNormClass`, `NonarchAddGroupSeminorm`, `funLike`, `instInhabited`, `instMax`, `instOneOfDecidableEq`, `instPartialOrder`, `instSMul`, `instSemilatticeSup`, `instSupSet`, `instZero`, `toZeroHom`, `NonarchAddGroupSeminormClass`	70
Theorems `addGroupNormClass`, `add_apply`, `apply_one`, `coe_add`, `coe_le_coe`, `coe_lt_coe`, `coe_sup`, `eq_zero_of_map_eq_zero'`, `ext`, `ext_iff`, `le_def`, `lt_def`, `sup_apply`, `toAddGroupSeminorm_eq_coe`, `addGroupSeminormClass`, `add_apply`, `add_bddBelow_range_add`, `add_comp`, `add_le'`, `apply_one`, `coe_add`, `coe_comp`, `coe_iSup_apply`, `coe_le_coe`, `coe_lt_coe`, `coe_sSup_apply`, `coe_sSup_apply'`, `coe_smul`, `coe_sup`, `coe_zero`, `comp_add_le`, `comp_apply`, `comp_assoc`, `comp_id`, `comp_mono`, `comp_zero`, `ext`, `ext_iff`, `inf_apply`, `isScalarTower`, `le_def`, `lt_def`, `map_zero'`, `neg'`, `sSup_of_not_bddAbove`, `smul_apply`, `smul_sup`, `sup_apply`, `toFun_eq_coe`, `zero_apply`, `zero_comp`, `add_apply`, `apply_one`, `coe_add`, `coe_le_coe`, `coe_lt_coe`, `coe_sup`, `eq_one_of_map_eq_zero'`, `ext`, `ext_iff`, `groupNormClass`, `le_def`, `lt_def`, `sup_apply`, `toGroupSeminorm_eq_coe`, `add_apply`, `add_comp`, `apply_one`, `coe_add`, `coe_comp`, `coe_iSup_apply`, `coe_le_coe`, `coe_lt_coe`, `coe_sSup_apply`, `coe_sSup_apply'`, `coe_smul`, `coe_sup`, `coe_zero`, `comp_apply`, `comp_assoc`, `comp_id`, `comp_mono`, `comp_mul_le`, `comp_zero`, `ext`, `ext_iff`, `groupSeminormClass`, `inf_apply`, `instIsScalarTowerOfReal`, `inv'`, `le_def`, `lt_def`, `map_one'`, `mul_bddBelow_range_add`, `mul_le'`, `sSup_of_not_bddAbove`, `smul_apply`, `smul_sup`, `sup_apply`, `toFun_eq_coe`, `zero_apply`, `zero_comp`, `apply_one`, `coe_le_coe`, `coe_lt_coe`, `coe_sup`, `eq_zero_of_map_eq_zero'`, `ext`, `ext_iff`, `le_def`, `lt_def`, `nonarchAddGroupNormClass`, `sup_apply`, `toNonarchAddGroupSeminorm_eq_coe`, `eq_zero_of_map_eq_zero`, `toAddGroupNormClass`, `toNonarchAddGroupSeminormClass`, `add_bddBelow_range_add`, `add_le_max'`, `apply_one`, `coe_iSup_apply`, `coe_le_coe`, `coe_lt_coe`, `coe_sSup_apply`, `coe_sSup_apply'`, `coe_smul`, `coe_sup`, `coe_zero`, `ext`, `ext_iff`, `instIsScalarTowerOfReal`, `le_def`, `lt_def`, `neg'`, `nonarchAddGroupSeminormClass`, `sSup_of_not_bddAbove`, `smul_apply`, `smul_sup`, `sup_apply`, `toZeroHom_eq_coe`, `zero_apply`, `map_neg_eq_map'`, `map_zero`, `toAddGroupSeminormClass`, `toNonarchimedeanHomClass`, `map_sub_le_max`	146
Total	216

AddGroupNorm

Definitions

Name	Category	Theorems
`funLike` 📖	CompOp	12 math math: `add_apply`, `coe_le_coe`, `ext_iff`, `coe_add`, `coe_sup`, `le_def`, `apply_one`, `sup_apply`, `addGroupNormClass`, `lt_def`, `coe_lt_coe`, `toAddGroupSeminorm_eq_coe`
`instAdd` 📖	CompOp	2 math math: `add_apply`, `coe_add`
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	2 math math: `coe_sup`, `sup_apply`
`instOne` 📖	CompOp	1 math math: `apply_one`
`instPartialOrder` 📖	CompOp	4 math math: `coe_le_coe`, `le_def`, `lt_def`, `coe_lt_coe`
`instSemilatticeSup` 📖	CompOp	—
`toAddGroupSeminorm` 📖	CompOp	1 math math: `toAddGroupSeminorm_eq_coe`
`toOne` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addGroupNormClass` 📖	mathematical	—	`AddGroupNormClass` `AddGroupNorm` `Real` `Real.instAddCommMonoid` `Real.partialOrder` `funLike`	—	`AddGroupSeminorm.add_le'` `AddGroupSeminorm.map_zero'` `AddGroupSeminorm.neg'` `eq_zero_of_map_eq_zero'`
`add_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupNorm` `Real` `funLike` `instAdd` `Real.instAdd`	—	—
`apply_one` 📖	mathematical	—	`DFunLike.coe` `AddGroupNorm` `Real` `funLike` `instOne` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Real.instZero` `Real.instOne`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `AddGroupNorm` `Real` `funLike` `instAdd` `Pi.instAdd` `Real.instAdd`	—	—
`coe_le_coe` 📖	mathematical	—	`Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `AddGroupNorm` `funLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_lt_coe` 📖	mathematical	—	`Preorder.toLT` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `AddGroupNorm` `funLike` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `AddGroupNorm` `Real` `funLike` `instMax` `Pi.instMaxForall_mathlib` `Real.instMax`	—	—
`eq_zero_of_map_eq_zero'` 📖	mathematical	`AddGroupSeminorm.toFun` `toAddGroupSeminorm` `Real` `Real.instZero`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`ext` 📖	—	`DFunLike.coe` `AddGroupNorm` `Real` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `AddGroupNorm` `Real` `funLike`	—	`ext`
`le_def` 📖	mathematical	—	`AddGroupNorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `funLike`	—	—
`lt_def` 📖	mathematical	—	`AddGroupNorm` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `funLike`	—	—
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupNorm` `Real` `funLike` `instMax` `Real.instMax`	—	—
`toAddGroupSeminorm_eq_coe` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `AddGroupSeminorm.funLike` `toAddGroupSeminorm` `AddGroupNorm` `funLike`	—	—

AddGroupSeminorm

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	9 math math: `comp_id`, `comp_zero`, `comp_mono`, `zero_comp`, `comp_assoc`, `comp_add_le`, `comp_apply`, `coe_comp`, `add_comp`
`funLike` 📖	CompOp	28 math math: `ext_iff`, `toFun_eq_coe`, `coe_lt_coe`, `add_bddBelow_range_add`, `coe_add`, `coe_iSup_apply`, `sup_apply`, `coe_le_coe`, `coe_sSup_apply`, `apply_one`, `RingSeminorm.toFun_eq_coe`, `coe_sSup_apply'`, `comp_apply`, `coe_smul`, `add_apply`, `addGroupSeminormClass`, `coe_comp`, `le_def`, `QuotientAddGroup.norm_eq_addGroupSeminorm`, `smul_apply`, `MulRingSeminorm.toFun_eq_coe`, `zero_apply`, `coe_zero`, `coe_normAddGroupSeminorm`, `lt_def`, `inf_apply`, `AddGroupNorm.toAddGroupSeminorm_eq_coe`, `coe_sup`
`instAdd` 📖	CompOp	4 math math: `coe_add`, `comp_add_le`, `add_apply`, `add_comp`
`instInhabited` 📖	CompOp	—
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	3 math math: `sup_apply`, `smul_sup`, `coe_sup`
`instMin` 📖	CompOp	1 math math: `inf_apply`
`instPartialOrder` 📖	CompOp	5 math math: `coe_lt_coe`, `coe_le_coe`, `comp_add_le`, `le_def`, `lt_def`
`instSupSet` 📖	CompOp	4 math math: `coe_iSup_apply`, `coe_sSup_apply`, `coe_sSup_apply'`, `sSup_of_not_bddAbove`
`instZeroAddGroupSeminorm` 📖	CompOp	5 math math: `comp_zero`, `zero_comp`, `zero_apply`, `coe_zero`, `sSup_of_not_bddAbove`
`semilatticeSup` 📖	CompOp	—
`toFun` 📖	CompOp	16 math math: `MulRingSeminorm.map_mul'`, `neg'`, `NormedRing.toRingNorm_toFun`, `MulAlgebraNorm.toFun_eq_coe`, `Seminorm.smul'`, `toFun_eq_coe`, `AlgebraNorm.smul'`, `AlgebraNorm.toFun_eq_coe`, `normRingNorm_toFun`, `RingSeminorm.mul_le'`, `RingNorm.toFun_eq_coe`, `add_le'`, `MulRingNorm.toFun_eq_coe`, `map_zero'`, `MulRingSeminorm.map_one'`, `MulAlgebraNorm.smul'`
`toOne` 📖	CompOp	1 math math: `apply_one`
`toSMul` 📖	CompOp	4 math math: `coe_smul`, `smul_sup`, `isScalarTower`, `smul_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addGroupSeminormClass` 📖	mathematical	—	`AddGroupSeminormClass` `AddGroupSeminorm` `Real` `Real.instAddCommMonoid` `Real.partialOrder` `funLike`	—	`add_le'` `map_zero'` `neg'`
`add_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike` `instAdd` `Real.instAdd`	—	—
`add_bddBelow_range_add` 📖	mathematical	—	`BddBelow` `Real` `Real.instLE` `Set.range` `Real.instAdd` `DFunLike.coe` `AddGroupSeminorm` `AddCommGroup.toAddGroup` `funLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `NonnegHomClass.apply_nonneg` `AddGroupSeminormClass.toNonnegHomClass` `addGroupSeminormClass`
`add_comp` 📖	mathematical	—	`comp` `AddGroupSeminorm` `instAdd`	—	`ext`
`add_le'` 📖	mathematical	—	`Real` `Real.instLE` `toFun` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Real.instAdd`	—	—
`apply_one` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike` `toOne` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Real.instZero` `Real.instOne`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike` `instAdd` `Pi.instAdd` `Real.instAdd`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike` `comp` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	—	—
`coe_iSup_apply` 📖	mathematical	`BddAbove` `AddGroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set.range`	`DFunLike.coe` `Real` `funLike` `iSup` `instSupSet` `Real.instSupSet`	—	`sSup_range` `coe_sSup_apply` `Function.Surjective.iSup_congr` `Set.rangeFactorization_surjective`
`coe_le_coe` 📖	mathematical	—	`Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `AddGroupSeminorm` `funLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_lt_coe` 📖	mathematical	—	`Preorder.toLT` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `AddGroupSeminorm` `funLike` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_sSup_apply` 📖	mathematical	`BddAbove` `AddGroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Real` `funLike` `SupSet.sSup` `instSupSet` `iSup` `Set.Elem` `Real.instSupSet` `Set` `Set.instMembership`	—	—
`coe_sSup_apply'` 📖	mathematical	`BddAbove` `AddGroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Real` `funLike` `SupSet.sSup` `instSupSet` `Real.instSupSet` `Set.image`	—	`coe_sSup_apply` `sSup_range` `Set.ext` `Set.mem_range` `Set.mem_image`
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike` `toSMul` `Function.hasSMul`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike` `instMax` `Pi.instMaxForall_mathlib` `Real.instMax`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike` `instZeroAddGroupSeminorm` `Pi.instZero` `Real.instZero`	—	—
`comp_add_le` 📖	mathematical	—	`AddGroupSeminorm` `AddCommGroup.toAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `comp` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.add` `AddCommGroup.toAddCommMonoid` `instAdd`	—	`SubadditiveHomClass.map_add_le_add` `AddGroupSeminormClass.toSubadditiveHomClass` `addGroupSeminormClass`
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike` `comp` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	—	—
`comp_assoc` 📖	mathematical	—	`comp` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`ext`
`comp_id` 📖	mathematical	—	`comp` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`ext`
`comp_mono` 📖	mathematical	`AddGroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`comp`	—	—
`comp_zero` 📖	mathematical	—	`comp` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instZeroAddMonoidHom` `AddGroupSeminorm` `instZeroAddGroupSeminorm`	—	`ext` `AddGroupSeminormClass.map_zero` `addGroupSeminormClass`
`ext` 📖	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike`	—	`ext`
`inf_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `AddCommGroup.toAddGroup` `Real` `funLike` `instMin` `iInf` `Real.instInfSet` `Real.instAdd` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `AddGroupSeminorm` `toSMul`	—	`ext` `smul_assoc`
`le_def` 📖	mathematical	—	`AddGroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `funLike`	—	—
`lt_def` 📖	mathematical	—	`AddGroupSeminorm` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `funLike`	—	—
`map_zero'` 📖	mathematical	—	`toFun` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Real` `Real.instZero`	—	—
`neg'` 📖	mathematical	—	`toFun` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`sSup_of_not_bddAbove` 📖	mathematical	`BddAbove` `AddGroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SupSet.sSup` `instSupSet` `instZeroAddGroupSeminorm`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike` `toSMul`	—	—
`smul_sup` 📖	mathematical	—	`AddGroupSeminorm` `toSMul` `instMax`	—	`smul_one_smul` `mul_max_of_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `NNReal.coe_nonneg` `ext`
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike` `instMax` `Real.instMax`	—	—
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `AddGroupSeminorm` `Real` `funLike`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `Real` `funLike` `instZeroAddGroupSeminorm` `Real.instZero`	—	—
`zero_comp` 📖	mathematical	—	`comp` `AddGroupSeminorm` `instZeroAddGroupSeminorm`	—	`ext`

GroupNorm

Definitions

Name	Category	Theorems
`funLike` 📖	CompOp	13 math math: `le_def`, `toGroupSeminorm_eq_coe`, `coe_normGroupNorm`, `coe_sup`, `coe_le_coe`, `groupNormClass`, `coe_add`, `apply_one`, `add_apply`, `ext_iff`, `lt_def`, `coe_lt_coe`, `sup_apply`
`instAdd` 📖	CompOp	2 math math: `coe_add`, `add_apply`
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	2 math math: `coe_sup`, `sup_apply`
`instPartialOrder` 📖	CompOp	4 math math: `le_def`, `coe_le_coe`, `lt_def`, `coe_lt_coe`
`instSemilatticeSup` 📖	CompOp	—
`toGroupSeminorm` 📖	CompOp	1 math math: `toGroupSeminorm_eq_coe`
`toOne` 📖	CompOp	1 math math: `apply_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `GroupNorm` `Real` `funLike` `instAdd` `Real.instAdd`	—	—
`apply_one` 📖	mathematical	—	`DFunLike.coe` `GroupNorm` `Real` `funLike` `toOne` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Real.instZero` `Real.instOne`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `GroupNorm` `Real` `funLike` `instAdd` `Pi.instAdd` `Real.instAdd`	—	—
`coe_le_coe` 📖	mathematical	—	`Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `GroupNorm` `funLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_lt_coe` 📖	mathematical	—	`Preorder.toLT` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `GroupNorm` `funLike` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `GroupNorm` `Real` `funLike` `instMax` `Pi.instMaxForall_mathlib` `Real.instMax`	—	—
`eq_one_of_map_eq_zero'` 📖	mathematical	`GroupSeminorm.toFun` `toGroupSeminorm` `Real` `Real.instZero`	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`ext` 📖	—	`DFunLike.coe` `GroupNorm` `Real` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `GroupNorm` `Real` `funLike`	—	`ext`
`groupNormClass` 📖	mathematical	—	`GroupNormClass` `GroupNorm` `Real` `Real.instAddCommMonoid` `Real.partialOrder` `funLike`	—	`GroupSeminorm.mul_le'` `GroupSeminorm.map_one'` `GroupSeminorm.inv'` `eq_one_of_map_eq_zero'`
`le_def` 📖	mathematical	—	`GroupNorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `funLike`	—	—
`lt_def` 📖	mathematical	—	`GroupNorm` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `funLike`	—	—
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `GroupNorm` `Real` `funLike` `instMax` `Real.instMax`	—	—
`toGroupSeminorm_eq_coe` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `GroupSeminorm.funLike` `toGroupSeminorm` `GroupNorm` `funLike`	—	—

GroupSeminorm

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	9 math math: `comp_assoc`, `comp_mul_le`, `add_comp`, `zero_comp`, `coe_comp`, `comp_zero`, `comp_id`, `comp_apply`, `comp_mono`
`funLike` 📖	CompOp	26 math math: `apply_one`, `coe_sup`, `GroupNorm.toGroupSeminorm_eq_coe`, `coe_iSup_apply`, `lt_def`, `ext_iff`, `inf_apply`, `coe_comp`, `smul_apply`, `zero_apply`, `coe_zero`, `coe_sSup_apply'`, `toFun_eq_coe`, `comp_apply`, `coe_smul`, `groupSeminormClass`, `coe_le_coe`, `le_def`, `coe_normGroupSeminorm`, `coe_add`, `QuotientGroup.norm_eq_groupSeminorm`, `coe_sSup_apply`, `add_apply`, `mul_bddBelow_range_add`, `sup_apply`, `coe_lt_coe`
`instAdd` 📖	CompOp	4 math math: `comp_mul_le`, `add_comp`, `coe_add`, `add_apply`
`instInhabited` 📖	CompOp	—
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	3 math math: `coe_sup`, `smul_sup`, `sup_apply`
`instMin` 📖	CompOp	1 math math: `inf_apply`
`instPartialOrder` 📖	CompOp	5 math math: `comp_mul_le`, `lt_def`, `coe_le_coe`, `le_def`, `coe_lt_coe`
`instSMul` 📖	CompOp	4 math math: `smul_sup`, `smul_apply`, `coe_smul`, `instIsScalarTowerOfReal`
`instSupSet` 📖	CompOp	4 math math: `coe_iSup_apply`, `sSup_of_not_bddAbove`, `coe_sSup_apply'`, `coe_sSup_apply`
`instZeroGroupSeminorm` 📖	CompOp	5 math math: `sSup_of_not_bddAbove`, `zero_comp`, `comp_zero`, `zero_apply`, `coe_zero`
`semilatticeSup` 📖	CompOp	—
`toFun` 📖	CompOp	4 math math: `inv'`, `toFun_eq_coe`, `map_one'`, `mul_le'`
`toOne` 📖	CompOp	1 math math: `apply_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike` `instAdd` `Real.instAdd`	—	—
`add_comp` 📖	mathematical	—	`comp` `GroupSeminorm` `instAdd`	—	`ext`
`apply_one` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike` `toOne` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Real.instZero` `Real.instOne`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike` `instAdd` `Pi.instAdd` `Real.instAdd`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike` `comp` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	—	—
`coe_iSup_apply` 📖	mathematical	`BddAbove` `GroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set.range`	`DFunLike.coe` `Real` `funLike` `iSup` `instSupSet` `Real.instSupSet`	—	`sSup_range` `coe_sSup_apply` `Function.Surjective.iSup_congr` `Set.rangeFactorization_surjective`
`coe_le_coe` 📖	mathematical	—	`Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `GroupSeminorm` `funLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_lt_coe` 📖	mathematical	—	`Preorder.toLT` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `GroupSeminorm` `funLike` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_sSup_apply` 📖	mathematical	`BddAbove` `GroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Real` `funLike` `SupSet.sSup` `instSupSet` `iSup` `Set.Elem` `Real.instSupSet` `Set` `Set.instMembership`	—	—
`coe_sSup_apply'` 📖	mathematical	`BddAbove` `GroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Real` `funLike` `SupSet.sSup` `instSupSet` `Real.instSupSet` `Set.image`	—	`coe_sSup_apply` `sSup_range` `Set.ext`
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike` `instSMul` `Function.hasSMul`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike` `instMax` `Pi.instMaxForall_mathlib` `Real.instMax`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike` `instZeroGroupSeminorm` `Pi.instZero` `Real.instZero`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike` `comp` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	—	—
`comp_assoc` 📖	mathematical	—	`comp` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`ext`
`comp_id` 📖	mathematical	—	`comp` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`ext`
`comp_mono` 📖	mathematical	`GroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`comp`	—	—
`comp_mul_le` 📖	mathematical	—	`GroupSeminorm` `CommGroup.toGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `comp` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.mul` `CommGroup.toCommMonoid` `instAdd`	—	`MulLEAddHomClass.map_mul_le_add` `GroupSeminormClass.toMulLEAddHomClass` `groupSeminormClass`
`comp_zero` 📖	mathematical	—	`comp` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instOneMonoidHom` `GroupSeminorm` `instZeroGroupSeminorm`	—	`ext` `GroupSeminormClass.map_one_eq_zero` `groupSeminormClass`
`ext` 📖	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike`	—	`ext`
`groupSeminormClass` 📖	mathematical	—	`GroupSeminormClass` `GroupSeminorm` `Real` `Real.instAddCommMonoid` `Real.partialOrder` `funLike`	—	`mul_le'` `map_one'` `inv'`
`inf_apply` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `CommGroup.toGroup` `Real` `funLike` `instMin` `iInf` `Real.instInfSet` `Real.instAdd` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	—
`instIsScalarTowerOfReal` 📖	mathematical	—	`IsScalarTower` `GroupSeminorm` `instSMul`	—	`ext` `smul_assoc`
`inv'` 📖	mathematical	—	`toFun` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`le_def` 📖	mathematical	—	`GroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `funLike`	—	—
`lt_def` 📖	mathematical	—	`GroupSeminorm` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `funLike`	—	—
`map_one'` 📖	mathematical	—	`toFun` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Real` `Real.instZero`	—	—
`mul_bddBelow_range_add` 📖	mathematical	—	`BddBelow` `Real` `Real.instLE` `Set.range` `Real.instAdd` `DFunLike.coe` `GroupSeminorm` `CommGroup.toGroup` `funLike` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `NonnegHomClass.apply_nonneg` `GroupSeminormClass.toNonnegHomClass` `groupSeminormClass`
`mul_le'` 📖	mathematical	—	`Real` `Real.instLE` `toFun` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Real.instAdd`	—	—
`sSup_of_not_bddAbove` 📖	mathematical	`BddAbove` `GroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SupSet.sSup` `instSupSet` `instZeroGroupSeminorm`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike` `instSMul`	—	—
`smul_sup` 📖	mathematical	—	`GroupSeminorm` `instSMul` `instMax`	—	`smul_one_smul` `mul_max_of_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `NNReal.coe_nonneg` `ext`
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike` `instMax` `Real.instMax`	—	—
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `GroupSeminorm` `Real` `funLike`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `GroupSeminorm` `Real` `funLike` `instZeroGroupSeminorm` `Real.instZero`	—	—
`zero_comp` 📖	mathematical	—	`comp` `GroupSeminorm` `instZeroGroupSeminorm`	—	`ext`

NonarchAddGroupNorm

Definitions

Name	Category	Theorems
`funLike` 📖	CompOp	10 math math: `le_def`, `coe_le_coe`, `lt_def`, `ext_iff`, `coe_sup`, `apply_one`, `sup_apply`, `coe_lt_coe`, `toNonarchAddGroupSeminorm_eq_coe`, `nonarchAddGroupNormClass`
`instInhabitedOfDecidableEq` 📖	CompOp	—
`instMax` 📖	CompOp	2 math math: `coe_sup`, `sup_apply`
`instOneOfDecidableEq` 📖	CompOp	1 math math: `apply_one`
`instPartialOrder` 📖	CompOp	4 math math: `le_def`, `coe_le_coe`, `lt_def`, `coe_lt_coe`
`instSemilatticeSup` 📖	CompOp	—
`toNonarchAddGroupSeminorm` 📖	CompOp	1 math math: `toNonarchAddGroupSeminorm_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_one` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupNorm` `Real` `funLike` `instOneOfDecidableEq` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Real.instZero` `Real.instOne`	—	—
`coe_le_coe` 📖	mathematical	—	`Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `NonarchAddGroupNorm` `funLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_lt_coe` 📖	mathematical	—	`Preorder.toLT` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `NonarchAddGroupNorm` `funLike` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupNorm` `Real` `funLike` `instMax` `Pi.instMaxForall_mathlib` `Real.instMax`	—	—
`eq_zero_of_map_eq_zero'` 📖	—	`ZeroHom.toFun` `Real` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Real.instZero` `NonarchAddGroupSeminorm.toZeroHom` `toNonarchAddGroupSeminorm`	—	—	—
`ext` 📖	—	`DFunLike.coe` `NonarchAddGroupNorm` `Real` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupNorm` `Real` `funLike`	—	`ext`
`le_def` 📖	mathematical	—	`NonarchAddGroupNorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `funLike`	—	—
`lt_def` 📖	mathematical	—	`NonarchAddGroupNorm` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `funLike`	—	—
`nonarchAddGroupNormClass` 📖	mathematical	—	`NonarchAddGroupNormClass` `NonarchAddGroupNorm` `funLike`	—	`NonarchAddGroupSeminorm.add_le_max'` `ZeroHom.map_zero'` `NonarchAddGroupSeminorm.neg'` `eq_zero_of_map_eq_zero'`
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupNorm` `Real` `funLike` `instMax` `Real.instMax`	—	—
`toNonarchAddGroupSeminorm_eq_coe` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupSeminorm` `Real` `NonarchAddGroupSeminorm.funLike` `toNonarchAddGroupSeminorm` `NonarchAddGroupNorm` `funLike`	—	—

NonarchAddGroupNormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_map_eq_zero` 📖	mathematical	`DFunLike.coe` `Real` `Real.instZero`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`toAddGroupNormClass` 📖	mathematical	—	`AddGroupNormClass` `Real` `Real.instAddCommMonoid` `Real.partialOrder`	—	`AddGroupSeminormClass.toSubadditiveHomClass` `NonarchAddGroupSeminormClass.toAddGroupSeminormClass` `toNonarchAddGroupSeminormClass` `NonarchAddGroupSeminormClass.map_zero` `NonarchAddGroupSeminormClass.map_neg_eq_map'` `eq_zero_of_map_eq_zero`
`toNonarchAddGroupSeminormClass` 📖	mathematical	—	`NonarchAddGroupSeminormClass`	—	—

NonarchAddGroupSeminorm

Definitions

Name	Category	Theorems
`funLike` 📖	CompOp	19 math math: `coe_iSup_apply`, `coe_sup`, `coe_zero`, `coe_smul`, `lt_def`, `coe_lt_coe`, `smul_apply`, `ext_iff`, `nonarchAddGroupSeminormClass`, `apply_one`, `zero_apply`, `add_bddBelow_range_add`, `toZeroHom_eq_coe`, `le_def`, `sup_apply`, `coe_le_coe`, `coe_sSup_apply'`, `NonarchAddGroupNorm.toNonarchAddGroupSeminorm_eq_coe`, `coe_sSup_apply`
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	3 math math: `smul_sup`, `coe_sup`, `sup_apply`
`instOneOfDecidableEq` 📖	CompOp	1 math math: `apply_one`
`instPartialOrder` 📖	CompOp	4 math math: `lt_def`, `coe_lt_coe`, `le_def`, `coe_le_coe`
`instSMul` 📖	CompOp	4 math math: `smul_sup`, `coe_smul`, `smul_apply`, `instIsScalarTowerOfReal`
`instSemilatticeSup` 📖	CompOp	—
`instSupSet` 📖	CompOp	4 math math: `coe_iSup_apply`, `sSup_of_not_bddAbove`, `coe_sSup_apply'`, `coe_sSup_apply`
`instZero` 📖	CompOp	3 math math: `coe_zero`, `sSup_of_not_bddAbove`, `zero_apply`
`toZeroHom` 📖	CompOp	3 math math: `toZeroHom_eq_coe`, `add_le_max'`, `neg'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_bddBelow_range_add` 📖	mathematical	—	`BddBelow` `Real` `Real.instLE` `Set.range` `Real.instAdd` `DFunLike.coe` `NonarchAddGroupSeminorm` `AddCommGroup.toAddGroup` `funLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `NonnegHomClass.apply_nonneg` `AddGroupSeminormClass.toNonnegHomClass` `NonarchAddGroupSeminormClass.toAddGroupSeminormClass` `nonarchAddGroupSeminormClass`
`add_le_max'` 📖	mathematical	—	`Real` `Real.instLE` `ZeroHom.toFun` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Real.instZero` `toZeroHom` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Real.instMax`	—	—
`apply_one` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupSeminorm` `Real` `funLike` `instOneOfDecidableEq` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Real.instZero` `Real.instOne`	—	—
`coe_iSup_apply` 📖	mathematical	`BddAbove` `NonarchAddGroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set.range`	`DFunLike.coe` `Real` `funLike` `iSup` `instSupSet` `Real.instSupSet`	—	`sSup_range` `coe_sSup_apply` `Function.Surjective.iSup_congr` `Set.rangeFactorization_surjective`
`coe_le_coe` 📖	mathematical	—	`Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `NonarchAddGroupSeminorm` `funLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_lt_coe` 📖	mathematical	—	`Preorder.toLT` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `NonarchAddGroupSeminorm` `funLike` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`coe_sSup_apply` 📖	mathematical	`BddAbove` `NonarchAddGroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Real` `funLike` `SupSet.sSup` `instSupSet` `iSup` `Set.Elem` `Real.instSupSet` `Set` `Set.instMembership`	—	—
`coe_sSup_apply'` 📖	mathematical	`BddAbove` `NonarchAddGroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Real` `funLike` `SupSet.sSup` `instSupSet` `Real.instSupSet` `Set.image`	—	`coe_sSup_apply` `sSup_range` `Set.ext`
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupSeminorm` `Real` `funLike` `instSMul` `Function.hasSMul`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupSeminorm` `Real` `funLike` `instMax` `Pi.instMaxForall_mathlib` `Real.instMax`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupSeminorm` `Real` `funLike` `instZero` `Pi.instZero` `Real.instZero`	—	—
`ext` 📖	—	`DFunLike.coe` `NonarchAddGroupSeminorm` `Real` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupSeminorm` `Real` `funLike`	—	`ext`
`instIsScalarTowerOfReal` 📖	mathematical	—	`IsScalarTower` `NonarchAddGroupSeminorm` `instSMul`	—	`ext` `smul_assoc`
`le_def` 📖	mathematical	—	`NonarchAddGroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Pi.hasLe` `Real` `Real.instLE` `DFunLike.coe` `funLike`	—	—
`lt_def` 📖	mathematical	—	`NonarchAddGroupSeminorm` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Pi.preorder` `Real` `Real.instPreorder` `DFunLike.coe` `funLike`	—	—
`neg'` 📖	mathematical	—	`ZeroHom.toFun` `Real` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Real.instZero` `toZeroHom` `NegZeroClass.toNeg`	—	—
`nonarchAddGroupSeminormClass` 📖	mathematical	—	`NonarchAddGroupSeminormClass` `NonarchAddGroupSeminorm` `funLike`	—	`add_le_max'` `ZeroHom.map_zero'` `neg'`
`sSup_of_not_bddAbove` 📖	mathematical	`BddAbove` `NonarchAddGroupSeminorm` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SupSet.sSup` `instSupSet` `instZero`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupSeminorm` `Real` `funLike` `instSMul`	—	—
`smul_sup` 📖	mathematical	—	`NonarchAddGroupSeminorm` `instSMul` `instMax`	—	`smul_one_smul` `mul_max_of_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `NNReal.coe_nonneg` `ext`
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupSeminorm` `Real` `funLike` `instMax` `Real.instMax`	—	—
`toZeroHom_eq_coe` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `Real` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Real.instZero` `ZeroHom.funLike` `toZeroHom` `NonarchAddGroupSeminorm` `funLike`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `NonarchAddGroupSeminorm` `Real` `funLike` `instZero` `Real.instZero`	—	—

NonarchAddGroupSeminormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_neg_eq_map'` 📖	mathematical	—	`DFunLike.coe` `Real` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`map_zero` 📖	mathematical	—	`DFunLike.coe` `Real` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Real.instZero`	—	—
`toAddGroupSeminormClass` 📖	mathematical	—	`AddGroupSeminormClass` `Real` `Real.instAddCommMonoid` `Real.partialOrder`	—	`le_trans` `NonarchimedeanHomClass.map_add_le_max` `toNonarchimedeanHomClass` `max_le` `le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `map_zero` `sub_self` `map_sub_le_max` `max_self` `le_refl` `le_add_of_nonneg_left` `covariant_swap_add_of_covariant_add` `map_neg_eq_map'`
`toNonarchimedeanHomClass` 📖	mathematical	—	`NonarchimedeanHomClass` `Real` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Real.linearOrder`	—	—

(root)

Definitions

Name	Category	Theorems
`AddGroupNorm` 📖	CompData	12 math math: `AddGroupNorm.add_apply`, `AddGroupNorm.coe_le_coe`, `AddGroupNorm.ext_iff`, `AddGroupNorm.coe_add`, `AddGroupNorm.coe_sup`, `AddGroupNorm.le_def`, `AddGroupNorm.apply_one`, `AddGroupNorm.sup_apply`, `AddGroupNorm.addGroupNormClass`, `AddGroupNorm.lt_def`, `AddGroupNorm.coe_lt_coe`, `AddGroupNorm.toAddGroupSeminorm_eq_coe`
`AddGroupSeminorm` 📖	CompData	31 math math: `AddGroupSeminorm.ext_iff`, `AddGroupSeminorm.comp_zero`, `AddGroupSeminorm.toFun_eq_coe`, `AddGroupSeminorm.coe_lt_coe`, `AddGroupSeminorm.add_bddBelow_range_add`, `AddGroupSeminorm.zero_comp`, `AddGroupSeminorm.coe_add`, `AddGroupSeminorm.sup_apply`, `AddGroupSeminorm.coe_le_coe`, `AddGroupSeminorm.apply_one`, `RingSeminorm.toFun_eq_coe`, `AddGroupSeminorm.comp_add_le`, `AddGroupSeminorm.comp_apply`, `AddGroupSeminorm.coe_smul`, `AddGroupSeminorm.add_apply`, `AddGroupSeminorm.smul_sup`, `AddGroupSeminorm.isScalarTower`, `AddGroupSeminorm.addGroupSeminormClass`, `AddGroupSeminorm.coe_comp`, `AddGroupSeminorm.le_def`, `QuotientAddGroup.norm_eq_addGroupSeminorm`, `AddGroupSeminorm.smul_apply`, `MulRingSeminorm.toFun_eq_coe`, `AddGroupSeminorm.zero_apply`, `AddGroupSeminorm.coe_zero`, `coe_normAddGroupSeminorm`, `AddGroupSeminorm.lt_def`, `AddGroupSeminorm.inf_apply`, `AddGroupNorm.toAddGroupSeminorm_eq_coe`, `AddGroupSeminorm.coe_sup`, `AddGroupSeminorm.add_comp`
`GroupNorm` 📖	CompData	13 math math: `GroupNorm.le_def`, `GroupNorm.toGroupSeminorm_eq_coe`, `coe_normGroupNorm`, `GroupNorm.coe_sup`, `GroupNorm.coe_le_coe`, `GroupNorm.groupNormClass`, `GroupNorm.coe_add`, `GroupNorm.apply_one`, `GroupNorm.add_apply`, `GroupNorm.ext_iff`, `GroupNorm.lt_def`, `GroupNorm.coe_lt_coe`, `GroupNorm.sup_apply`
`GroupSeminorm` 📖	CompData	29 math math: `GroupSeminorm.apply_one`, `GroupSeminorm.comp_mul_le`, `GroupSeminorm.coe_sup`, `GroupNorm.toGroupSeminorm_eq_coe`, `GroupSeminorm.lt_def`, `GroupSeminorm.add_comp`, `GroupSeminorm.smul_sup`, `GroupSeminorm.ext_iff`, `GroupSeminorm.zero_comp`, `GroupSeminorm.inf_apply`, `GroupSeminorm.coe_comp`, `GroupSeminorm.smul_apply`, `GroupSeminorm.comp_zero`, `GroupSeminorm.zero_apply`, `GroupSeminorm.coe_zero`, `GroupSeminorm.toFun_eq_coe`, `GroupSeminorm.comp_apply`, `GroupSeminorm.coe_smul`, `GroupSeminorm.groupSeminormClass`, `GroupSeminorm.coe_le_coe`, `GroupSeminorm.le_def`, `coe_normGroupSeminorm`, `GroupSeminorm.coe_add`, `QuotientGroup.norm_eq_groupSeminorm`, `GroupSeminorm.add_apply`, `GroupSeminorm.instIsScalarTowerOfReal`, `GroupSeminorm.mul_bddBelow_range_add`, `GroupSeminorm.sup_apply`, `GroupSeminorm.coe_lt_coe`
`NonarchAddGroupNorm` 📖	CompData	10 math math: `NonarchAddGroupNorm.le_def`, `NonarchAddGroupNorm.coe_le_coe`, `NonarchAddGroupNorm.lt_def`, `NonarchAddGroupNorm.ext_iff`, `NonarchAddGroupNorm.coe_sup`, `NonarchAddGroupNorm.apply_one`, `NonarchAddGroupNorm.sup_apply`, `NonarchAddGroupNorm.coe_lt_coe`, `NonarchAddGroupNorm.toNonarchAddGroupSeminorm_eq_coe`, `NonarchAddGroupNorm.nonarchAddGroupNormClass`
`NonarchAddGroupNormClass` 📖	CompData	1 math math: `NonarchAddGroupNorm.nonarchAddGroupNormClass`
`NonarchAddGroupSeminorm` 📖	CompData	18 math math: `NonarchAddGroupSeminorm.smul_sup`, `NonarchAddGroupSeminorm.coe_sup`, `NonarchAddGroupSeminorm.coe_zero`, `NonarchAddGroupSeminorm.coe_smul`, `NonarchAddGroupSeminorm.lt_def`, `NonarchAddGroupSeminorm.coe_lt_coe`, `NonarchAddGroupSeminorm.smul_apply`, `NonarchAddGroupSeminorm.ext_iff`, `NonarchAddGroupSeminorm.nonarchAddGroupSeminormClass`, `NonarchAddGroupSeminorm.apply_one`, `NonarchAddGroupSeminorm.zero_apply`, `NonarchAddGroupSeminorm.add_bddBelow_range_add`, `NonarchAddGroupSeminorm.toZeroHom_eq_coe`, `NonarchAddGroupSeminorm.le_def`, `NonarchAddGroupSeminorm.instIsScalarTowerOfReal`, `NonarchAddGroupSeminorm.sup_apply`, `NonarchAddGroupSeminorm.coe_le_coe`, `NonarchAddGroupNorm.toNonarchAddGroupSeminorm_eq_coe`
`NonarchAddGroupSeminormClass` 📖	CompData	2 math math: `NonarchAddGroupSeminorm.nonarchAddGroupSeminormClass`, `NonarchAddGroupNormClass.toNonarchAddGroupSeminormClass`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_sub_le_max` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Real.instMax`	—	`sub_eq_add_neg` `NonarchAddGroupSeminormClass.map_neg_eq_map'` `NonarchimedeanHomClass.map_add_le_max` `NonarchAddGroupSeminormClass.toNonarchimedeanHomClass`

---

← Back to Index