Ultra

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

Statistics

Metric	Count
Definitions `ball_openAddSubgroup`, `ball_openSubgroup`, `closedBall_openAddSubgroup`, `closedBall_openSubgroup`	4
Theorems `norm_prod_le_sup'_norm`, `norm_sum_le_sup'_norm`, `nnnorm_prod_le_sup_nnnorm`, `nnnorm_sum_le_sup_nnnorm`, `exists_norm_finset_prod_le`, `exists_norm_finset_prod_le_of_nonempty`, `exists_norm_finset_sum_le`, `exists_norm_finset_sum_le_of_nonempty`, `exists_norm_multiset_prod_le`, `exists_norm_multiset_sum_le`, `isNonarchimedean_nnnorm`, `isNonarchimedean_norm`, `isUltrametricDist_iff_isNonarchimedean_nnnorm`, `isUltrametricDist_iff_isNonarchimedean_norm`, `isUltrametricDist_of_forall_nnnorm_add_le_max_nnnorm`, `isUltrametricDist_of_forall_nnnorm_mul_le_max_nnnorm`, `isUltrametricDist_of_forall_norm_add_le_max_norm`, `isUltrametricDist_of_forall_norm_mul_le_max_norm`, `isUltrametricDist_of_isNonarchimedean_nnnorm`, `isUltrametricDist_of_isNonarchimedean_norm`, `nnnorm_add_eq_max_of_nnnorm_ne_nnnorm`, `nnnorm_add_le_max`, `nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div`, `nnnorm_eq_of_add_nnnorm_lt_max`, `nnnorm_eq_of_mul_nnnorm_lt_max`, `nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm`, `nnnorm_mul_le_max`, `nnnorm_nsmul_le`, `nnnorm_pow_le`, `nnnorm_prod_eq_sup_of_pairwise_ne`, `nnnorm_prod_le_of_forall_le`, `nnnorm_sub_eq_max_of_nnnorm_sub_ne_nnnorm_sub`, `nnnorm_sum_eq_sup_of_pairwise_ne`, `nnnorm_sum_le_of_forall_le`, `nnnorm_tprod_le`, `nnnorm_tprod_le_of_forall_le`, `nnnorm_tsum_le`, `nnnorm_tsum_le_of_forall_le`, `nnnorm_zpow_le`, `nnnorm_zsmul_le`, `nonarchimedeanAddGroup`, `nonarchimedeanGroup`, `norm_add_eq_max_of_norm_ne_norm`, `norm_add_le_max`, `norm_div_eq_max_of_norm_div_ne_norm_div`, `norm_eq_of_add_norm_lt_max`, `norm_eq_of_mul_norm_lt_max`, `norm_mul_eq_max_of_norm_ne_norm`, `norm_mul_le_max`, `norm_nsmul_le`, `norm_pow_le`, `norm_prod_eq_sup'_of_pairwise_ne`, `norm_prod_le_of_forall_le_of_nonempty`, `norm_prod_le_of_forall_le_of_nonneg`, `norm_sub_eq_max_of_norm_sub_ne_norm_sub`, `norm_sum_eq_sup'_of_pairwise_ne`, `norm_sum_le_of_forall_le_of_nonempty`, `norm_sum_le_of_forall_le_of_nonneg`, `norm_tprod_le`, `norm_tprod_le_of_forall_le`, `norm_tprod_le_of_forall_le_of_nonneg`, `norm_tsum_le`, `norm_tsum_le_of_forall_le`, `norm_tsum_le_of_forall_le_of_nonneg`, `norm_zpow_le`, `norm_zsmul_le`	66
Total	70

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nnnorm_prod_le_sup_nnnorm` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `SeminormedCommGroup.toSeminormedGroup` `prod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup` `sup` `instSemilatticeSupNNReal` `NNReal.instOrderBot`	—	`eq_empty_or_nonempty` `nnnorm_one'` `sup_empty` `bot_eq_zero'` `NNReal.instCanonicallyOrderedAdd` `sup'_eq_sup` `Nonempty.norm_prod_le_sup'_norm`
`nnnorm_sum_le_sup_nnnorm` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `sup` `instSemilatticeSupNNReal` `NNReal.instOrderBot`	—	`eq_empty_or_nonempty` `nnnorm_zero` `sup_empty` `bot_eq_zero'` `NNReal.instCanonicallyOrderedAdd` `le_refl` `sup'_eq_sup` `le_sup'_iff` `Nonempty.norm_sum_le_sup'_norm`

Finset.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_prod_le_sup'_norm` 📖	mathematical	`Finset.Nonempty`	`Real` `Real.instLE` `Norm.norm` `SeminormedCommGroup.toNorm` `Finset.prod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup` `Finset.sup'` `Real.instSemilatticeSup`	—	`cons_induction` `Finset.prod_singleton` `Finset.prod_cons` `LE.le.trans` `IsUltrametricDist.norm_mul_le_max` `Eq.le` `max_eq_left` `max_eq_right` `le_total`
`norm_sum_le_sup'_norm` 📖	mathematical	`Finset.Nonempty`	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.sup'` `Real.instSemilatticeSup`	—	`Finset.le_sup'_iff` `cons_induction` `Finset.mem_singleton` `Finset.sum_singleton` `le_refl` `Finset.mem_cons` `Finset.sum_cons` `LE.le.trans` `IsUltrametricDist.norm_add_le_max` `Eq.le` `max_eq_left` `max_eq_right` `le_total`

IsUltrametricDist

Definitions

Name	Category	Theorems
`ball_openAddSubgroup` 📖	CompOp	—
`ball_openSubgroup` 📖	CompOp	—
`closedBall_openAddSubgroup` 📖	CompOp	—
`closedBall_openSubgroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_norm_finset_prod_le` 📖	mathematical	—	`Finset` `Finset.instMembership` `Real` `Real.instLE` `Norm.norm` `SeminormedCommGroup.toNorm` `Finset.prod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup`	—	`Finset.eq_empty_or_nonempty` `norm_one'` `exists_norm_finset_prod_le_of_nonempty`
`exists_norm_finset_prod_le_of_nonempty` 📖	mathematical	`Finset.Nonempty`	`Finset` `Finset.instMembership` `Real` `Real.instLE` `Norm.norm` `SeminormedCommGroup.toNorm` `Finset.prod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup`	—	`Finset.exists_mem_eq_sup'` `LE.le.trans` `Finset.Nonempty.norm_prod_le_sup'_norm` `le_of_eq`
`exists_norm_finset_sum_le` 📖	mathematical	—	`Finset` `Finset.instMembership` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`Finset.eq_empty_or_nonempty` `Finset.not_nonempty_empty` `Finset.notMem_empty` `norm_zero` `norm_nonneg` `exists_norm_finset_sum_le_of_nonempty`
`exists_norm_finset_sum_le_of_nonempty` 📖	mathematical	`Finset.Nonempty`	`Finset` `Finset.instMembership` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`Finset.exists_mem_eq_sup'` `LE.le.trans` `Finset.Nonempty.norm_sum_le_sup'_norm` `le_of_eq`
`exists_norm_multiset_prod_le` 📖	mathematical	—	`Multiset` `Multiset.instMembership` `Real` `Real.instLE` `Norm.norm` `SeminormedCommGroup.toNorm` `Multiset.prod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup` `Multiset.map`	—	`Multiset.induction_on` `norm_one'` `Multiset.map_cons` `Multiset.prod_cons` `le_trans` `norm_mul_le_max` `max_le` `le_refl` `eq_or_ne` `Multiset.prod_singleton` `LT.lt.le`
`exists_norm_multiset_sum_le` 📖	mathematical	—	`Multiset` `Multiset.instMembership` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Multiset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Multiset.map`	—	`Multiset.induction_on` `Multiset.notMem_zero` `norm_zero` `norm_nonneg` `Multiset.cons_ne_zero` `Multiset.mem_cons` `Multiset.map_cons` `Multiset.sum_cons` `le_trans` `norm_add_le_max` `max_le` `le_refl` `eq_or_ne` `Multiset.singleton_ne_zero` `Multiset.mem_singleton` `Multiset.sum_singleton` `LT.lt.le` `not_le`
`isNonarchimedean_nnnorm` 📖	mathematical	—	`IsNonarchimedean` `Real` `Real.linearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NNReal.toReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`isNonarchimedean_norm`
`isNonarchimedean_norm` 📖	mathematical	—	`IsNonarchimedean` `Real` `Real.linearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`dist_zero` `SeminormedAddGroup.dist_eq` `zero_sub` `norm_neg` `sub_add_cancel_left` `dist_triangle_max`
`isUltrametricDist_iff_isNonarchimedean_nnnorm` 📖	mathematical	—	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsNonarchimedean` `Real` `Real.linearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NNReal.toReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`isNonarchimedean_norm` `isUltrametricDist_of_isNonarchimedean_norm`
`isUltrametricDist_iff_isNonarchimedean_norm` 📖	mathematical	—	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsNonarchimedean` `Real` `Real.linearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`isNonarchimedean_norm` `isUltrametricDist_of_isNonarchimedean_norm`
`isUltrametricDist_of_forall_nnnorm_add_le_max_nnnorm` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `NNReal.instMax`	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedAddGroup.toPseudoMetricSpace`	—	`isUltrametricDist_of_forall_norm_add_le_max_norm`
`isUltrametricDist_of_forall_nnnorm_mul_le_max_nnnorm` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SeminormedGroup.toGroup` `NNReal.instMax`	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedGroup.toPseudoMetricSpace`	—	`isUltrametricDist_of_forall_norm_mul_le_max_norm`
`isUltrametricDist_of_forall_norm_add_le_max_norm` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddGroup.toNorm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `Real.instMax`	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedAddGroup.toPseudoMetricSpace`	—	`dist_eq_norm_sub` `le_max_iff` `sub_add_sub_cancel`
`isUltrametricDist_of_forall_norm_mul_le_max_norm` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedGroup.toNorm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SeminormedGroup.toGroup` `Real.instMax`	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedGroup.toPseudoMetricSpace`	—	`dist_eq_norm_div` `div_mul_div_cancel`
`isUltrametricDist_of_isNonarchimedean_nnnorm` 📖	mathematical	`IsNonarchimedean` `NNReal` `NNReal.instLinearOrder` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm`	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedAddGroup.toPseudoMetricSpace`	—	`isUltrametricDist_of_forall_nnnorm_add_le_max_nnnorm`
`isUltrametricDist_of_isNonarchimedean_norm` 📖	mathematical	`IsNonarchimedean` `Real` `Real.linearOrder` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `Norm.norm` `SeminormedAddGroup.toNorm`	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedAddGroup.toPseudoMetricSpace`	—	`isUltrametricDist_of_forall_norm_add_le_max_norm`
`nnnorm_add_eq_max_of_nnnorm_ne_nnnorm` 📖	mathematical	—	`NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `NNReal` `NNReal.instMax`	—	`NNReal.coe_max` `norm_add_eq_max_of_norm_ne_norm` `NNReal.coe_injective`
`nnnorm_add_le_max` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `NNReal.instMax`	—	`norm_add_le_max`
`nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div` 📖	mathematical	—	`NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `SeminormedGroup.toGroup` `NNReal` `NNReal.instMax`	—	`NNReal.coe_max` `norm_div_eq_max_of_norm_div_ne_norm_div` `NNReal.coe_injective`
`nnnorm_eq_of_add_nnnorm_lt_max` 📖	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `NNReal.instMax`	—	—	`not_ne_iff` `LT.lt.ne` `nnnorm_add_eq_max_of_nnnorm_ne_nnnorm`
`nnnorm_eq_of_mul_nnnorm_lt_max` 📖	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SeminormedGroup.toGroup` `NNReal.instMax`	—	—	`not_ne_iff` `LT.lt.ne` `nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm`
`nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm` 📖	mathematical	—	`NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SeminormedGroup.toGroup` `NNReal` `NNReal.instMax`	—	`NNReal.coe_max` `norm_mul_eq_max_of_norm_ne_norm` `NNReal.coe_injective`
`nnnorm_mul_le_max` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SeminormedGroup.toGroup` `NNReal.instMax`	—	`norm_mul_le_max`
`nnnorm_nsmul_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup`	—	`zero_nsmul` `nnnorm_zero` `zero_le` `NNReal.instCanonicallyOrderedAdd` `add_nsmul` `one_nsmul` `sup_of_le_right` `nnnorm_add_le_max`
`nnnorm_pow_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SeminormedGroup.toGroup`	—	`pow_zero` `nnnorm_one'` `NNReal.instCanonicallyOrderedAdd` `pow_add` `pow_one` `sup_of_le_right` `nnnorm_mul_le_max`
`nnnorm_prod_eq_sup_of_pairwise_ne` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `NNReal` `NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `SeminormedCommGroup.toSeminormedGroup`	`Finset.prod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup` `Finset.sup` `instSemilatticeSupNNReal` `NNReal.instOrderBot`	—	`Finset.cons_induction` `nnnorm_one'` `Finset.sup_empty` `bot_eq_zero'` `NNReal.instCanonicallyOrderedAdd` `Finset.eq_empty_or_nonempty` `Finset.prod_singleton` `Finset.sup_singleton` `Set.Pairwise.mono` `Finset.coe_cons` `Finset.exists_mem_eq_sup` `Finset.prod_cons` `nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm` `Finset.sup_cons`
`nnnorm_prod_le_of_forall_le` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `SeminormedCommGroup.toSeminormedGroup`	`Finset.prod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup`	—	`LE.le.trans` `Finset.nnnorm_prod_le_sup_nnnorm` `Finset.sup_le`
`nnnorm_sub_eq_max_of_nnnorm_sub_ne_nnnorm_sub` 📖	mathematical	—	`NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `NNReal` `NNReal.instMax`	—	`NNReal.coe_max` `norm_sub_eq_max_of_norm_sub_ne_norm_sub` `NNReal.coe_injective`
`nnnorm_sum_eq_sup_of_pairwise_ne` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `NNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.sup` `instSemilatticeSupNNReal` `NNReal.instOrderBot`	—	`Finset.cons_induction` `nnnorm_zero` `Finset.sup_empty` `bot_eq_zero'` `NNReal.instCanonicallyOrderedAdd` `Finset.eq_empty_or_nonempty` `Finset.sum_singleton` `Finset.sup_singleton` `Set.Pairwise.mono` `Finset.coe_cons` `Set.subset_insert` `Finset.exists_mem_eq_sup` `Finset.sum_cons` `nnnorm_add_eq_max_of_nnnorm_ne_nnnorm` `Finset.sup_cons`
`nnnorm_sum_le_of_forall_le` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`LE.le.trans` `Finset.nnnorm_sum_le_sup_nnnorm` `Finset.sup_le`
`nnnorm_tprod_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `SeminormedCommGroup.toSeminormedGroup` `tprod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `NNReal.instConditionallyCompleteLinearOrderBot`	—	`NNReal.coe_iSup` `norm_tprod_le`
`nnnorm_tprod_le_of_forall_le` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `SeminormedCommGroup.toSeminormedGroup`	`tprod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional`	—	`LE.le.trans` `nnnorm_tprod_le` `ciSup_le'`
`nnnorm_tsum_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `tsum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `NNReal.instConditionallyCompleteLinearOrderBot`	—	`NNReal.coe_le_coe` `NNReal.coe_iSup` `norm_tsum_le`
`nnnorm_tsum_le_of_forall_le` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`tsum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional`	—	`LE.le.trans` `nnnorm_tsum_le` `ciSup_le'`
`nnnorm_zpow_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedGroup.toNNNorm` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `SeminormedGroup.toGroup`	—	`zpow_natCast` `nnnorm_pow_le` `zpow_negSucc` `nnnorm_inv'`
`nnnorm_zsmul_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup`	—	`natCast_zsmul` `nnnorm_nsmul_le` `negSucc_zsmul` `nnnorm_neg`
`nonarchimedeanAddGroup` 📖	mathematical	—	`NonarchimedeanAddGroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `Metric.mem_nhds_iff`
`nonarchimedeanGroup` 📖	mathematical	—	`NonarchimedeanGroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedCommGroup.toPseudoMetricSpace`	—	`SeminormedCommGroup.toIsTopologicalGroup`
`norm_add_eq_max_of_norm_ne_norm` 📖	mathematical	—	`Norm.norm` `SeminormedAddGroup.toNorm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `Real` `Real.instMax`	—	`sub_neg_eq_add` `dist_eq_norm_sub` `dist_eq_max_of_dist_ne_dist` `dist_zero_right` `dist_zero` `norm_neg` `dist_zero_left`
`norm_add_le_max` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedAddGroup.toNorm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `Real.instMax`	—	`le_max_iff` `dist_eq_norm_sub` `sub_neg_eq_add` `sub_zero` `zero_add` `dist_triangle_max`
`norm_div_eq_max_of_norm_div_ne_norm_div` 📖	mathematical	—	`Norm.norm` `SeminormedGroup.toNorm` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `SeminormedGroup.toGroup` `Real` `Real.instMax`	—	`div_mul_div_cancel` `norm_mul_eq_max_of_norm_ne_norm`
`norm_eq_of_add_norm_lt_max` 📖	—	`Real` `Real.instLT` `Norm.norm` `SeminormedAddGroup.toNorm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `Real.instMax`	—	—	`not_ne_iff` `LT.lt.ne` `norm_add_eq_max_of_norm_ne_norm`
`norm_eq_of_mul_norm_lt_max` 📖	—	`Real` `Real.instLT` `Norm.norm` `SeminormedGroup.toNorm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SeminormedGroup.toGroup` `Real.instMax`	—	—	`not_ne_iff` `LT.lt.ne` `norm_mul_eq_max_of_norm_ne_norm`
`norm_mul_eq_max_of_norm_ne_norm` 📖	mathematical	—	`Norm.norm` `SeminormedGroup.toNorm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SeminormedGroup.toGroup` `Real` `Real.instMax`	—	`div_inv_eq_mul` `dist_eq_norm_div` `dist_eq_max_of_dist_ne_dist` `dist_one_right` `dist_one` `norm_inv'` `dist_one_left`
`norm_mul_le_max` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedGroup.toNorm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SeminormedGroup.toGroup` `Real.instMax`	—	`dist_eq_norm_div` `div_inv_eq_mul` `div_one` `one_mul` `dist_triangle_max`
`norm_nsmul_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedAddGroup.toNorm` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup`	—	`nnnorm_nsmul_le`
`norm_pow_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedGroup.toNorm` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SeminormedGroup.toGroup`	—	`nnnorm_pow_le`
`norm_prod_eq_sup'_of_pairwise_ne` 📖	mathematical	`Finset.Nonempty` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Real` `Norm.norm` `SeminormedCommGroup.toNorm`	`Finset.prod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup` `Finset.sup'` `Real.instSemilatticeSup`	—	`coe_nnnorm'` `nnnorm_prod_eq_sup_of_pairwise_ne` `Finset.sup'_eq_sup` `Finset.comp_sup'_eq_sup'_comp`
`norm_prod_le_of_forall_le_of_nonempty` 📖	mathematical	`Finset.Nonempty` `Real` `Real.instLE` `Norm.norm` `SeminormedCommGroup.toNorm`	`Finset.prod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup`	—	`LE.le.trans` `Finset.Nonempty.norm_prod_le_sup'_norm` `Finset.sup'_le`
`norm_prod_le_of_forall_le_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `SeminormedCommGroup.toNorm`	`Finset.prod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup`	—	`CanLift.prf` `NNReal.canLift` `nnnorm_prod_le_of_forall_le`
`norm_sub_eq_max_of_norm_sub_ne_norm_sub` 📖	mathematical	—	`Norm.norm` `SeminormedAddGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `Real` `Real.instMax`	—	`sub_add_sub_cancel` `norm_add_eq_max_of_norm_ne_norm`
`norm_sum_eq_sup'_of_pairwise_ne` 📖	mathematical	`Finset.Nonempty` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Real` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.sup'` `Real.instSemilatticeSup`	—	`coe_nnnorm` `nnnorm_sum_eq_sup_of_pairwise_ne` `Finset.sup'_eq_sup` `Finset.comp_sup'_eq_sup'_comp`
`norm_sum_le_of_forall_le_of_nonempty` 📖	mathematical	`Finset.Nonempty` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`LE.le.trans` `Finset.Nonempty.norm_sum_le_sup'_norm` `Finset.sup'_le`
`norm_sum_le_of_forall_le_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`CanLift.prf` `NNReal.canLift` `nnnorm_sum_le_of_forall_le`
`norm_tprod_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedCommGroup.toNorm` `tprod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional` `iSup` `Real.instSupSet`	—	`isEmpty_or_nonempty` `tprod_empty` `norm_one'` `Real.iSup_of_isEmpty` `Filter.Tendsto.bddAbove_range_of_cofinite` `BoundedLENhdsClass.of_closedIciTopology` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Filter.Tendsto.norm'` `Multipliable.tendsto_cofinite_one` `NonarchimedeanGroup.toIsTopologicalGroup` `nonarchimedeanGroup` `le_of_tendsto'` `instClosedIicTopology` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `Multipliable.hasProd` `norm_prod_le_of_forall_le_of_nonneg` `le_ciSup_of_le` `norm_nonneg'` `le_ciSup` `tprod_eq_one_of_not_multipliable` `Real.iSup_of_not_bddAbove` `le_refl`
`norm_tprod_le_of_forall_le` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedCommGroup.toNorm`	`tprod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional`	—	`LE.le.trans` `norm_tprod_le` `ciSup_le`
`norm_tprod_le_of_forall_le_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `SeminormedCommGroup.toNorm`	`tprod` `CommGroup.toCommMonoid` `SeminormedCommGroup.toCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional`	—	`isEmpty_or_nonempty` `tprod_empty` `norm_one'` `norm_tprod_le_of_forall_le`
`norm_tsum_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `tsum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional` `iSup` `Real.instSupSet`	—	`isEmpty_or_nonempty` `tsum_empty` `norm_zero` `Real.iSup_of_isEmpty` `le_refl` `Filter.Tendsto.bddAbove_range_of_cofinite` `BoundedLENhdsClass.of_closedIciTopology` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Filter.Tendsto.norm` `Summable.tendsto_cofinite_zero` `NonarchimedeanAddGroup.toIsTopologicalAddGroup` `nonarchimedeanAddGroup` `le_of_tendsto'` `instClosedIicTopology` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `Summable.hasSum` `norm_sum_le_of_forall_le_of_nonneg` `le_ciSup_of_le` `norm_nonneg` `le_ciSup` `tsum_eq_zero_of_not_summable` `Real.iSup_of_not_bddAbove`
`norm_tsum_le_of_forall_le` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`tsum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional`	—	`LE.le.trans` `norm_tsum_le` `ciSup_le`
`norm_tsum_le_of_forall_le_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`tsum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional`	—	`isEmpty_or_nonempty` `tsum_empty` `norm_zero` `norm_tsum_le_of_forall_le`
`norm_zpow_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedGroup.toNorm` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `SeminormedGroup.toGroup`	—	`nnnorm_zpow_le`
`norm_zsmul_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedAddGroup.toNorm` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup`	—	`nnnorm_zsmul_le`

---

← Back to Index