Seminorm

📁 Source: Mathlib/Analysis/Seminorm.lean

Statistics

Metric	Count
Definitions Seminorm, ball, closedBall, coeFnAddMonoidHom, comp, instAdd, instAddCommMonoid, instAddMonoid, instConditionallyCompleteLattice, instDistribMulAction, instFunLike, instInf, instInhabited, instLattice, instModule, instMulAction, instOrderBot, instPartialOrder, instSMul, instSemilatticeSup, instSup, instSupSet, instZero, of, ofSMulLE, pullback, restrictScalars, toAddGroupSeminorm, SeminormClass, normSeminorm	30
Theorems absorbent_ball, absorbent_ball_zero, absorbent_closedBall, absorbent_closedBall_zero, add_apply, add_comp, balanced_ball_zero, balanced_closedBall_zero, ball_add_ball_subset, ball_antitone, ball_bot, ball_comp, ball_eq_emptyset, ball_finset_sup, ball_finset_sup', ball_finset_sup_eq_iInter, ball_mem_nhds, ball_mono, ball_norm_mul_subset, ball_smul, ball_smul_ball, ball_smul_closedBall, ball_subset_closedBall, ball_sup, ball_zero', ball_zero_absorbs_ball_zero, ball_zero_eq, ball_zero_eq_preimage_ball, bddAbove_iff, bddAbove_of_absorbent, bddAbove_range_iff, bddBelow_range_add, bot_eq_zero, bound_of_shell, bound_of_shell_smul, bound_of_shell_sup, closedBall_add_closedBall_subset, closedBall_antitone, closedBall_bot, closedBall_comp, closedBall_eq_biInter_ball, closedBall_eq_emptyset, closedBall_finset_sup, closedBall_finset_sup', closedBall_finset_sup_eq_iInter, closedBall_iSup, closedBall_mono, closedBall_smul, closedBall_smul_ball, closedBall_smul_closedBall, closedBall_sup, closedBall_zero', closedBall_zero_eq, closedBall_zero_eq_preimage_closedBall, coeFnAddMonoidHom_apply, coeFnAddMonoidHom_injective, coe_add, coe_bot, coe_comp, coe_iSup_eq, coe_le_coe, coe_lt_coe, coe_restrictScalars, coe_sSup_eq, coe_sSup_eq', coe_smul, coe_sup, coe_zero, comp_add_le, comp_apply, comp_comp, comp_id, comp_mono, comp_smul, comp_smul_apply, comp_zero, continuous, continuous', continuousAt_zero, continuousAt_zero', continuousAt_zero_of_forall, continuousAt_zero_of_forall', continuous_iff, continuous_of_continuousAt_zero, continuous_of_forall, continuous_of_forall', continuous_of_le, convexOn, convex_ball, convex_closedBall, exists_apply_eq_finset_sup, ext, ext_iff, finset_sup_apply, finset_sup_apply_le, finset_sup_apply_lt, finset_sup_le_sum, finset_sup_smul, iSup_apply, inf_apply, instIsOrderedCancelAddMonoid, instIsScalarTowerOfReal, instSeminormClass, le_def, le_finset_sup_apply, lt_def, mem_ball, mem_ball_self, mem_ball_zero, mem_closedBall, mem_closedBall_self, mem_closedBall_zero, neg_ball, neg_closedBall, neg_mem_ball_zero, neg_mem_closedBall_zero, norm_sub_map_le_sub, preimage_metric_ball, preimage_metric_closedBall, pullback_apply, rescale_to_shell, rescale_to_shell_zpow, restrictScalars_ball, restrictScalars_closedBall, sSup_apply, sSup_empty, smul', smul_apply, smul_ball_preimage, smul_ball_zero, smul_closedBall_preimage, smul_closedBall_subset, smul_closedBall_zero, smul_comp, smul_inf, smul_le_smul, smul_sup, sub_mem_ball, sub_mem_closedBall, sup_apply, uniformContinuous, uniformContinuous', uniformContinuous_of_continuousAt_zero, uniformContinuous_of_forall, uniformContinuous_of_forall', uniformSpace_eq_of_hasBasis, uniformity_eq_of_hasBasis, vadd_ball, vadd_closedBall, zero_apply, zero_comp, zero_or_exists_apply_eq_finset_sup, map_smul_eq_mul, toAddGroupSeminormClass, absorbent_ball, absorbent_ball_zero, balanced_ball_zero, balanced_closedBall_zero, ball_normSeminorm, closedBall_normSeminorm, coe_normSeminorm, rescale_to_shell, rescale_to_shell_semi_normed, rescale_to_shell_semi_normed_zpow, rescale_to_shell_zpow	165
Total	195

Seminorm

Definitions

Name	Category	Theorems
ball 📖	CompOp	51 math math: withSeminorms_iff_mem_nhds_isVonNBounded, mem_ball_zero, ball_sup, ball_smul_closedBall, WithSeminorms.mem_nhds_iff, neg_ball, ball_mono, ball_mem_nhds, ball_antitone, closedBall_smul_ball, ball_eq_emptyset, ball_norm_mul_subset, ball_smul, gaugeSeminorm_ball, ball_zero_eq_preimage_ball, balanced_ball_zero, restrictScalars_ball, gaugeSeminorm_ball_one, ball_normSeminorm, neg_mem_ball_zero, ball_zero', ball_add_ball_subset, WithSeminorms.isOpen_iff_mem_balls, mem_ball_self, convex_ball, continuous_iff, ball_zero_absorbs_ball_zero, ball_smul_ball, absorbent_ball_zero, ball_comp, mem_ball, gauge_ball, SeminormFamily.basisSets_singleton_mem, smul_ball_preimage, ball_subset_closedBall, closedBall_eq_biInter_ball, LinearMap.toSeminorm_ball_zero, vadd_ball, sub_mem_ball, smul_ball_zero, ball_finset_sup_eq_iInter, ball_finset_sup, gaugeSeminormFamily_ball, SeminormFamily.basisSets_mem, absorbent_ball, SeminormFamily.basisSets_iff, ball_zero_eq, ball_finset_sup', WithSeminorms.hasBasis_ball, ball_bot, WithSeminorms.hasBasis_zero_ball
closedBall 📖	CompOp	35 math math: absorbent_closedBall_zero, closedBall_zero', ball_smul_closedBall, restrictScalars_closedBall, closedBall_iSup, closedBall_antitone, mem_closedBall_zero, closedBall_zero_eq_preimage_closedBall, balanced_closedBall_zero, smul_closedBall_zero, closedBall_finset_sup, closedBall_mono, vadd_closedBall, closedBall_smul, neg_closedBall, closedBall_eq_emptyset, closedBall_sup, smul_closedBall_subset, closedBall_normSeminorm, smul_closedBall_preimage, closedBall_bot, ball_subset_closedBall, absorbent_closedBall, closedBall_eq_biInter_ball, closedBall_finset_sup', closedBall_zero_eq, mem_closedBall, closedBall_comp, convex_closedBall, mem_closedBall_self, closedBall_add_closedBall_subset, closedBall_finset_sup_eq_iInter, neg_mem_closedBall_zero, closedBall_smul_closedBall, sub_mem_closedBall
coeFnAddMonoidHom 📖	CompOp	2 math math: coeFnAddMonoidHom_apply, coeFnAddMonoidHom_injective
comp 📖	CompOp	27 math math: isBounded_const, smul_comp, SeminormFamily.comp_apply, pullback_apply, SeminormFamily.finset_sup_comp, WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm, comp_smul, comp_zero, LinearMap.toSeminorm_comp, add_comp, WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup, const_isBounded, PiTensorProduct.dualSeminorms_bounded, PiTensorProduct.injectiveSeminorm_apply, comp_apply, ball_comp, coe_comp, isBounded_sup, comp_id, comp_mono, comp_comp, zero_comp, comp_smul_apply, closedBall_comp, continuous_iff_continuous_comp, comp_add_le, PiTensorProduct.injectiveSeminorm_def
instAdd 📖	CompOp	4 math math: coe_add, add_comp, add_apply, comp_add_le
instAddCommMonoid 📖	CompOp	2 math math: instIsOrderedCancelAddMonoid, finset_sup_le_sum
instAddMonoid 📖	CompOp	3 math math: pullback_apply, coeFnAddMonoidHom_apply, coeFnAddMonoidHom_injective
instConditionallyCompleteLattice 📖	CompOp	—
instDistribMulAction 📖	CompOp	—
instFunLike 📖	CompOp	110 math math: SchwartzMap.norm_toLp_le_seminorm, instSeminormClass, mem_ball_zero, LinearMap.coe_toSeminorm, WithSeminorms.image_isVonNBounded_iff_seminorm_bounded, le_finset_sup_apply, norm_sub_map_le_sub, SchwartzMap.norm_le_seminorm, ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm, finset_sup_apply, SchwartzMap.seminorm_le_bound, ext_iff, uniformContinuous_of_forall, SeminormFamily.filter_eq_iInf, bddAbove_range_iff, continuous_of_forall', continuous', coe_le_coe, continuousAt_zero_of_forall', mem_closedBall_zero, lt_def, WithSeminorms.tendsto_nhds', PiTensorProduct.projectiveSeminorm_apply, ContDiffMapSupportedIn.seminorm_le_iff, closedBall_zero_eq_preimage_closedBall, convexOn, coe_restrictScalars, PiTensorProduct.projectiveSeminorm_tprod_le, WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm, ball_zero_eq_preimage_ball, rescale_to_shell_zpow, continuous, coe_smul, WithSeminorms.isVonNBounded_iff_seminorm_bddAbove, SchwartzMap.norm_iteratedFDeriv_le_seminorm, SchwartzMap.seminorm_le_bound', coe_sup, coe_add, PiTensorProduct.norm_eval_le_injectiveSeminorm, bddAbove_iff, continuousAt_zero', WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup, iSup_apply, WithSeminorms.tendsto_nhds, preimage_metric_closedBall, add_apply, PiTensorProduct.injectiveSeminorm_apply, ContDiffMapSupportedIn.seminorm_le_iff_withOrder, exists_apply_eq_finset_sup, WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded, SchwartzMap.integral_pow_mul_iteratedFDeriv_le, uniformContinuous, coe_bot, continuous_iff, WithSeminorms.continuous_seminorm, le_def, comp_apply, SchwartzMap.le_seminorm, SchwartzMap.eLpNorm_le_seminorm, ContDiffMapSupportedIn.norm_apply_le_seminorm, inf_apply, coe_sSup_eq, bddBelow_range_add, ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm_withOrder, ContDiffMapSupportedIn.seminorm_apply, WithSeminorms.tendsto_nhds_atTop, PolynormableSpace.withSeminorms', zero_or_exists_apply_eq_finset_sup, rescale_to_shell, continuousAt_zero_of_forall, SeminormFamily.withSeminorms_iff_nhds_eq_iInf, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, coe_normSeminorm, mem_ball, gauge_ball, coe_comp, PiTensorProduct.norm_eval_le_projectiveSeminorm, WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded, ContDiffMapSupportedIn.seminorm_postcompLM_le, smul_apply, coe_zero, LinearMap.toSeminorm_apply, SchwartzMap.seminorm_apply, SchwartzMap.le_seminorm', coeFnAddMonoidHom_apply, preimage_metric_ball, uniformContinuous', sup_apply, closedBall_zero_eq, LinearMap.toSeminormFamily_apply, coe_iSup_eq, PiTensorProduct.injectiveSeminorm_tprod_le, mem_closedBall, gaugeSeminorm_lt_one_of_isOpen, PolynormableSpace.withSeminorms, comp_smul_apply, coe_lt_coe, WithSeminorms.isVonNBounded_iff_seminorm_bounded, continuous_of_forall, ball_zero_eq, SchwartzMap.one_add_le_sup_seminorm_apply, continuous_iff_continuous_comp, uniformContinuous_of_forall', zero_apply, gaugeSeminorm_toFun, continuousAt_zero, sSup_apply, ContDiffMapSupportedIn.norm_toBoundedContinuousFunction, SchwartzMap.norm_pow_mul_le_seminorm, uniformity_eq_of_hasBasis
instInf 📖	CompOp	2 math math: smul_inf, inf_apply
instInhabited 📖	CompOp	—
instLattice 📖	CompOp	—
instModule 📖	CompOp	—
instMulAction 📖	CompOp	—
instOrderBot 📖	CompOp	38 math math: SchwartzMap.norm_toLp_le_seminorm, isBounded_const, le_finset_sup_apply, bot_eq_zero, finset_sup_apply, WithSeminorms.mem_nhds_iff, WithSeminorms.tendsto_nhds', SeminormFamily.finset_sup_comp, finset_sup_apply_lt, bound_of_continuous, closedBall_finset_sup, WithSeminorms.isOpen_iff_mem_balls, sSup_empty, exists_apply_eq_finset_sup, WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded, coe_bot, SchwartzMap.eLpNorm_le_seminorm, ContDiffMapSupportedIn.seminorm_eq_bot_of_gt, zero_or_exists_apply_eq_finset_sup, bound_of_shell_sup, WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded, finset_sup_smul, isBounded_sup, closedBall_bot, LinearMap.mem_span_iff_bound, WithSeminorms.partial_sups, ball_finset_sup_eq_iInter, ball_finset_sup, SeminormFamily.basisSets_mem, SeminormFamily.basisSets_iff, SchwartzMap.one_add_le_sup_seminorm_apply, WithSeminorms.hasBasis_ball, finset_sup_le_sum, finset_sup_apply_le, closedBall_finset_sup_eq_iInter, ball_bot, WithSeminorms.hasBasis_zero_ball, WithSeminorms.finset_sups
instPartialOrder 📖	CompOp	25 math math: isBounded_const, bot_eq_zero, bddAbove_range_iff, coe_le_coe, lt_def, bddAbove_of_absorbent, WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm, PiTensorProduct.injectiveSeminorm_le_projectiveSeminorm, bound_of_continuous, bddAbove_iff, WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup, const_isBounded, sSup_empty, PiTensorProduct.dualSeminorms_bounded, coe_bot, le_def, ContDiffMapSupportedIn.seminorm_eq_bot_of_gt, instIsOrderedCancelAddMonoid, isBounded_sup, closedBall_bot, LinearMap.mem_span_iff_bound, coe_lt_coe, finset_sup_le_sum, comp_add_le, ball_bot
instSMul 📖	CompOp	16 math math: isBounded_const, smul_sup, smul_comp, smul_inf, ball_smul, coe_smul, instIsScalarTowerOfReal, comp_smul, bound_of_continuous, const_isBounded, closedBall_smul, finset_sup_smul, isBounded_sup, smul_apply, LinearMap.mem_span_iff_bound, smul_le_smul
instSemilatticeSup 📖	CompOp	34 math math: SchwartzMap.norm_toLp_le_seminorm, isBounded_const, le_finset_sup_apply, finset_sup_apply, WithSeminorms.mem_nhds_iff, WithSeminorms.tendsto_nhds', SeminormFamily.finset_sup_comp, finset_sup_apply_lt, bound_of_continuous, closedBall_finset_sup, WithSeminorms.isOpen_iff_mem_balls, exists_apply_eq_finset_sup, WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded, SchwartzMap.eLpNorm_le_seminorm, zero_or_exists_apply_eq_finset_sup, bound_of_shell_sup, WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded, finset_sup_smul, isBounded_sup, closedBall_finset_sup', LinearMap.mem_span_iff_bound, WithSeminorms.partial_sups, ball_finset_sup_eq_iInter, ball_finset_sup, SeminormFamily.basisSets_mem, SeminormFamily.basisSets_iff, ball_finset_sup', SchwartzMap.one_add_le_sup_seminorm_apply, WithSeminorms.hasBasis_ball, finset_sup_le_sum, finset_sup_apply_le, closedBall_finset_sup_eq_iInter, WithSeminorms.hasBasis_zero_ball, WithSeminorms.finset_sups
instSup 📖	CompOp	5 math math: smul_sup, ball_sup, coe_sup, closedBall_sup, sup_apply
instSupSet 📖	CompOp	8 math math: closedBall_iSup, iSup_apply, sSup_empty, coe_sSup_eq', coe_sSup_eq, coe_iSup_eq, sSup_apply, PiTensorProduct.injectiveSeminorm_def
instZero 📖	CompOp	7 math math: bot_eq_zero, closedBall_zero', comp_zero, ball_zero', coe_zero, zero_comp, zero_apply
of 📖	CompOp	—
ofSMulLE 📖	CompOp	—
pullback 📖	CompOp	1 math math: pullback_apply
restrictScalars 📖	CompOp	3 math math: restrictScalars_closedBall, coe_restrictScalars, restrictScalars_ball
toAddGroupSeminorm 📖	CompOp	4 math math: smul', SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf, uniformSpace_eq_of_hasBasis, SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absorbent_ball 📖	mathematical	Real Real.instLT DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike	Absorbent PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace ball	—	Absorbent.mono absorbent_ball_zero sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mem_ball LE.le.trans_lt map_sub_le_add SeminormClass.toAddGroupSeminormClass instSeminormClass add_lt_of_lt_sub_right mem_ball_zero
absorbent_ball_zero 📖	mathematical	Real Real.instLT Real.instZero	Absorbent PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	absorbent_iff_forall_absorbs_singleton Absorbs.mono_right ball_zero_absorbs_ball_zero Set.singleton_subset_iff mem_ball_zero lt_add_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
absorbent_closedBall 📖	mathematical	Real Real.instLT DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike	Absorbent PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace closedBall	—	Absorbent.mono absorbent_closedBall_zero sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mem_closedBall LE.le.trans map_sub_le_add SeminormClass.toAddGroupSeminormClass instSeminormClass add_le_of_le_sub_right mem_closedBall_zero
absorbent_closedBall_zero 📖	mathematical	Real Real.instLT Real.instZero	Absorbent PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid closedBall NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Absorbent.mono absorbent_ball_zero ball_subset_closedBall
add_apply 📖	mathematical	—	DFunLike.coe Seminorm Real instFunLike instAdd Real.instAdd	—	—
add_comp 📖	mathematical	—	comp Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instAdd	—	ext
balanced_ball_zero 📖	mathematical	—	Balanced SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	mem_ball_zero SeminormClass.map_smul_eq_mul instSeminormClass mul_le_of_le_one_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass
balanced_closedBall_zero 📖	mathematical	—	Balanced SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid closedBall NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	mem_closedBall_zero SeminormClass.map_smul_eq_mul instSeminormClass mul_le_of_le_one_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass
ball_add_ball_subset 📖	mathematical	—	Set Set.instHasSubset Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid ball Real Real.instAdd	—	mem_ball add_sub_add_comm LE.le.trans_lt SubadditiveHomClass.map_add_le_add AddGroupSeminormClass.toSubadditiveHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add
ball_antitone 📖	mathematical	Seminorm AddCommGroup.toAddGroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	Set Set.instHasSubset ball	—	LE.le.trans_lt
ball_bot 📖	mathematical	Real Real.instLT Real.instZero	ball SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Bot.bot Seminorm OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot Set.univ	—	ball_zero'
ball_comp 📖	mathematical	—	ball SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid comp Set.preimage DFunLike.coe LinearMap LinearMap.instFunLike	—	Set.ext map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
ball_eq_emptyset 📖	mathematical	Real Real.instLE Real.instZero	ball SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Set Set.instEmptyCollection	—	Set.ext mem_ball Set.mem_empty_iff_false not_lt LE.le.trans NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass
ball_finset_sup 📖	mathematical	Real Real.instLT Real.instZero	ball SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Finset.sup Seminorm instSemilatticeSup instOrderBot Finset.inf Set Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instOrderTop	—	Finset.inf_eq_iInf ball_finset_sup_eq_iInter
ball_finset_sup' 📖	mathematical	Finset.Nonempty	ball Finset.sup' Seminorm AddCommGroup.toAddGroup instSemilatticeSup Finset.inf' Set Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	Finset.Nonempty.cons_induction Finset.cons_nonempty Finset.sup'_cons ball_sup Finset.inf'_cons
ball_finset_sup_eq_iInter 📖	mathematical	Real Real.instLT Real.instZero	ball SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Finset.sup Seminorm instSemilatticeSup instOrderBot Set.iInter Finset Finset.instMembership	—	CanLift.prf NNReal.canLift LT.lt.le Set.iInter_congr_Prop Set.iInter_setOf NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass finset_sup_apply Finset.sup_lt_iff
ball_mem_nhds 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike Real.instLT Real.instZero	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ball	—	Continuous.tendsto map_zero AddGroupSeminormClass.toZeroHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass ball_zero_eq Iio_mem_nhds instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal
ball_mono 📖	mathematical	Real Real.instLE	Set Set.instHasSubset ball	—	LT.lt.trans_le
ball_norm_mul_subset 📖	mathematical	—	Set Set.instHasSubset ball SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real Real.instMul Norm.norm NormedField.toNorm Set.smulSet	—	eq_or_ne norm_zero MulZeroClass.zero_mul ball_eq_emptyset le_rfl Set.empty_subset Set.mem_smul_set mem_ball_zero SeminormClass.map_smul_eq_mul instSeminormClass norm_inv mul_lt_mul_iff_right₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE norm_pos_iff mul_assoc div_eq_mul_inv div_self ne_of_gt one_mul smul_assoc IsScalarTower.left smul_eq_mul one_smul
ball_smul 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal	ball Seminorm AddCommGroup.toAddGroup instSMul Algebra.toSMul Real instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring CommSemiring.toSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NNReal.instMulActionOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid Real.instAddCommMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace DivInvMonoid.toDiv Real.instDivInvMonoid NNReal.toReal	—	Set.ext IsScalarTower.left mem_ball smul_apply NNReal.smul_def smul_eq_mul mul_comm lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing NNReal.coe_pos
ball_smul_ball 📖	mathematical	—	Set Set.instHasSubset Set.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Metric.ball SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real Real.instMul	—	eq_or_ne ball_eq_emptyset Set.smul_empty MulZeroClass.mul_zero Set.instReflSubset HasSubset.Subset.trans Set.instIsTransSubset Set.smul_subset_smul_left ball_subset_closedBall ball_smul_closedBall
ball_smul_closedBall 📖	mathematical	—	Set Set.instHasSubset Set.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Metric.ball SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing closedBall NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ball Real Real.instMul	—	SeminormClass.map_smul_eq_mul instSeminormClass mul_comm mul_lt_mul' IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg Ne.lt_or_gt LE.le.not_gt LE.le.trans NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass
ball_subset_closedBall 📖	mathematical	—	Set Set.instHasSubset ball closedBall	—	mem_closedBall LT.lt.le mem_ball
ball_sup 📖	mathematical	—	ball Seminorm AddCommGroup.toAddGroup instSup Set Set.instInter	—	—
ball_zero' 📖	mathematical	Real Real.instLT Real.instZero	ball Seminorm AddCommGroup.toAddGroup instZero Set.univ	—	Set.eq_univ_iff_forall ball.eq_1
ball_zero_absorbs_ball_zero 📖	mathematical	Real Real.instLT Real.instZero	Absorbs PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	exists_pos_lt_mul Real.instIsStrictOrderedRing Absorbs.of_norm smul_ball_zero norm_pos_iff LT.lt.trans_le mem_ball_zero LT.lt.trans mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing le_of_lt
ball_zero_eq 📖	mathematical	—	ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid setOf Real Real.instLT DFunLike.coe Seminorm AddCommGroup.toAddGroup instFunLike	—	Set.ext mem_ball_zero
ball_zero_eq_preimage_ball 📖	mathematical	—	ball SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.preimage Real DFunLike.coe Seminorm instFunLike Metric.ball Real.pseudoMetricSpace Real.instZero	—	ball_zero_eq preimage_metric_ball
bddAbove_iff 📖	mathematical	—	BddAbove Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder Pi.hasLe Real Real.instLE Set.image DFunLike.coe instFunLike	—	Set.forall_mem_image coe_sSup_eq' iSup_apply le_ciSup Set.forall_mem_range Set.mem_image_of_mem
bddAbove_of_absorbent 📖	mathematical	Absorbent PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid BddAbove Real Real.instLE Set.range DFunLike.coe Seminorm instFunLike	Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	bddAbove_range_iff Filter.Eventually.exists NormedField.nhdsNE_neBot Filter.Eventually.and eventually_mem_nhdsWithin Absorbent.eventually_nhdsNE_zero Set.forall_mem_range le_div_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff SeminormClass.map_smul_eq_mul instSeminormClass
bddAbove_range_iff 📖	mathematical	—	BddAbove Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder Set.range Real Real.instLE DFunLike.coe instFunLike	—	bddAbove_iff Set.range_comp bddAbove_range_pi
bddBelow_range_add 📖	mathematical	—	BddBelow Real Real.instLE Set.range Real.instAdd DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike SubNegMonoid.toSub	—	add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass
bot_eq_zero 📖	mathematical	—	Bot.bot Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot instZero	—	—
bound_of_shell 📖	—	Real Real.instLT Real.instZero Real.instOne Norm.norm NormedField.toNorm Real.instLE DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike Real.instMul	—	—	rescale_to_shell SeminormClass.map_smul_eq_mul instSeminormClass mul_left_comm mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff
bound_of_shell_smul 📖	—	Real Real.instLT Real.instZero Real.instOne Norm.norm NormedField.toNorm Real.instLE DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike NNReal instSMul Algebra.toSMul instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring CommSemiring.toSemiring IsScalarTower.left instSemiringNNReal NNReal.instMulActionOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace	—	—	IsScalarTower.left bound_of_shell
bound_of_shell_sup 📖	mathematical	Real Real.instLT Real.instZero Real.instOne Norm.norm NormedField.toNorm Real.instLE DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike NNReal instSMul Algebra.toSMul instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring CommSemiring.toSemiring IsScalarTower.left instSemiringNNReal NNReal.instMulActionOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Finset Finset.instMembership	Finset.sup instSemilatticeSup instOrderBot	—	IsScalarTower.left ne_of_gt LT.lt.trans_le Ne.lt_of_le NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass le_finset_sup_apply bound_of_shell_smul exists_apply_eq_finset_sup smul_apply LE.le.trans_lt
closedBall_add_closedBall_subset 📖	mathematical	—	Set Set.instHasSubset Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid closedBall Real Real.instAdd	—	mem_closedBall add_sub_add_comm LE.le.trans SubadditiveHomClass.map_add_le_add AddGroupSeminormClass.toSubadditiveHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
closedBall_antitone 📖	mathematical	Seminorm AddCommGroup.toAddGroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	Set Set.instHasSubset closedBall	—	LE.le.trans
closedBall_bot 📖	mathematical	Real Real.instLT Real.instZero	closedBall SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Bot.bot Seminorm OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot Set.univ	—	closedBall_zero'
closedBall_comp 📖	mathematical	—	closedBall SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid comp Set.preimage DFunLike.coe LinearMap LinearMap.instFunLike	—	Set.ext map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
closedBall_eq_biInter_ball 📖	mathematical	—	closedBall Set.iInter Real Real.instLT ball	—	Set.ext
closedBall_eq_emptyset 📖	mathematical	Real Real.instLT Real.instZero	closedBall SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Set Set.instEmptyCollection	—	Set.ext mem_closedBall Set.mem_empty_iff_false not_le LT.lt.trans_le NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass
closedBall_finset_sup 📖	mathematical	Real Real.instLE Real.instZero	closedBall SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Finset.sup Seminorm instSemilatticeSup instOrderBot Finset.inf Set Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instOrderTop	—	Finset.inf_eq_iInf closedBall_finset_sup_eq_iInter
closedBall_finset_sup' 📖	mathematical	Finset.Nonempty	closedBall Finset.sup' Seminorm AddCommGroup.toAddGroup instSemilatticeSup Finset.inf' Set Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	Finset.Nonempty.cons_induction Finset.cons_nonempty Finset.sup'_cons closedBall_sup Finset.inf'_cons
closedBall_finset_sup_eq_iInter 📖	mathematical	Real Real.instLE Real.instZero	closedBall SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Finset.sup Seminorm instSemilatticeSup instOrderBot Set.iInter Finset Finset.instMembership	—	CanLift.prf NNReal.canLift Set.iInter_congr_Prop Set.iInter_setOf NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass finset_sup_apply
closedBall_iSup 📖	mathematical	BddAbove Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder Set.range Real Real.instLT Real.instZero	closedBall iSup instSupSet Set.iInter	—	isEmpty_or_nonempty iSup_of_empty' Set.iInter_of_empty sSup_empty closedBall_bot Set.ext bddAbove_range_iff iSup_apply ciSup_le_iff
closedBall_mono 📖	mathematical	Real Real.instLE	Set Set.instHasSubset closedBall	—	LE.le.trans
closedBall_smul 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal	closedBall Seminorm AddCommGroup.toAddGroup instSMul Algebra.toSMul Real instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring CommSemiring.toSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NNReal.instMulActionOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid Real.instAddCommMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace DivInvMonoid.toDiv Real.instDivInvMonoid NNReal.toReal	—	Set.ext IsScalarTower.left mem_closedBall smul_apply NNReal.smul_def smul_eq_mul mul_comm le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing NNReal.coe_pos
closedBall_smul_ball 📖	mathematical	—	Set Set.instHasSubset Set.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Metric.closedBall SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real Real.instMul	—	SeminormClass.map_smul_eq_mul instSeminormClass mul_lt_mul' IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass Ne.lt_or_gt LE.le.not_gt LE.le.trans norm_nonneg
closedBall_smul_closedBall 📖	mathematical	—	Set Set.instHasSubset Set.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Metric.closedBall SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing closedBall NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real Real.instMul	—	SeminormClass.map_smul_eq_mul instSeminormClass mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass LE.le.trans norm_nonneg
closedBall_sup 📖	mathematical	—	closedBall Seminorm AddCommGroup.toAddGroup instSup Set Set.instInter	—	—
closedBall_zero' 📖	mathematical	Real Real.instLT Real.instZero	closedBall Seminorm AddCommGroup.toAddGroup instZero Set.univ	—	Set.eq_univ_of_subset ball_subset_closedBall ball_zero'
closedBall_zero_eq 📖	mathematical	—	closedBall NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid setOf Real Real.instLE DFunLike.coe Seminorm AddCommGroup.toAddGroup instFunLike	—	Set.ext mem_closedBall_zero
closedBall_zero_eq_preimage_closedBall 📖	mathematical	—	closedBall SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.preimage Real DFunLike.coe Seminorm instFunLike Metric.closedBall Real.pseudoMetricSpace Real.instZero	—	closedBall_zero_eq preimage_metric_closedBall
coeFnAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Seminorm AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid Pi.addZeroClass Real Real.instAddMonoid AddMonoidHom.instFunLike coeFnAddMonoidHom instFunLike	—	—
coeFnAddMonoidHom_injective 📖	mathematical	—	Seminorm DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid Pi.addZeroClass Real Real.instAddMonoid AddMonoidHom.instFunLike coeFnAddMonoidHom	—	DFunLike.coe_injective
coe_add 📖	mathematical	—	DFunLike.coe Seminorm Real instFunLike instAdd Pi.instAdd Real.instAdd	—	—
coe_bot 📖	mathematical	—	DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Real instFunLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot Pi.instZero Real.instZero	—	—
coe_comp 📖	mathematical	—	DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Real instFunLike comp LinearMap LinearMap.instFunLike	—	—
coe_iSup_eq 📖	mathematical	BddAbove Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder Set.range	DFunLike.coe Real instFunLike iSup instSupSet Pi.supSet Real.instSupSet	—	sSup_range coe_sSup_eq iSup_range'
coe_le_coe 📖	mathematical	—	Pi.hasLe Real Real.instLE DFunLike.coe Seminorm instFunLike Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	—
coe_lt_coe 📖	mathematical	—	Preorder.toLT Pi.preorder Real Real.instPreorder DFunLike.coe Seminorm instFunLike PartialOrder.toPreorder instPartialOrder	—	—
coe_restrictScalars 📖	mathematical	—	DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup Real instFunLike restrictScalars SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	—
coe_sSup_eq 📖	mathematical	BddAbove Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe Real instFunLike SupSet.sSup instSupSet iSup Set.Elem Pi.supSet Real.instSupSet Set Set.instMembership	—	coe_sSup_eq' bddAbove_iff
coe_sSup_eq' 📖	mathematical	BddAbove Pi.hasLe Real Real.instLE Set.image Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid DFunLike.coe instFunLike	SupSet.sSup instSupSet iSup Set.Elem Pi.supSet Real.instSupSet Set Set.instMembership	—	—
coe_smul 📖	mathematical	—	DFunLike.coe Seminorm Real instFunLike instSMul Function.hasSMul	—	—
coe_sup 📖	mathematical	—	DFunLike.coe Seminorm Real instFunLike instSup Pi.instMaxForall_mathlib Real.instMax	—	—
coe_zero 📖	mathematical	—	DFunLike.coe Seminorm Real instFunLike instZero Pi.instZero Real.instZero	—	—
comp_add_le 📖	mathematical	—	Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder comp LinearMap LinearMap.instAdd instAdd	—	SubadditiveHomClass.map_add_le_add AddGroupSeminormClass.toSubadditiveHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass
comp_apply 📖	mathematical	—	DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Real instFunLike comp LinearMap LinearMap.instFunLike	—	—
comp_comp 📖	mathematical	—	comp LinearMap.comp Ring.toSemiring SeminormedRing.toRing AddCommGroup.toAddCommMonoid	—	ext
comp_id 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing RingHomIsometric.ids LinearMap.id AddCommGroup.toAddCommMonoid	—	ext RingHomIsometric.ids
comp_mono 📖	mathematical	Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	comp	—	—
comp_smul 📖	mathematical	—	comp SeminormedCommRing.toSeminormedRing LinearMap Ring.toSemiring SeminormedRing.toRing CommSemiring.toSemiring CommRing.toCommSemiring SeminormedCommRing.toCommRing AddCommGroup.toAddCommMonoid LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid CommRing.toRing NNReal Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass instSMul Algebra.toSMul Real instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring IsScalarTower.left instSemiringNNReal NNReal.instMulActionOfReal Real.instMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	—	ext smulCommClass_self IsScalarTower.left comp_apply smul_apply LinearMap.smul_apply SeminormClass.map_smul_eq_mul instSeminormClass NNReal.smul_def coe_nnnorm smul_eq_mul
comp_smul_apply 📖	mathematical	—	DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Real instFunLike comp SeminormedCommRing.toSeminormedRing LinearMap CommSemiring.toSemiring CommRing.toCommSemiring SeminormedCommRing.toCommRing LinearMap.instSMul AddCommMonoid.toAddMonoid smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid CommRing.toRing Real.instMul Norm.norm SeminormedRing.toNorm LinearMap.instFunLike	—	SeminormClass.map_smul_eq_mul instSeminormClass
comp_zero 📖	mathematical	—	comp LinearMap Ring.toSemiring SeminormedRing.toRing AddCommGroup.toAddCommMonoid LinearMap.instZero Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instZero	—	ext map_zero AddGroupSeminormClass.toZeroHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass
continuous 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ball SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	continuous_of_continuousAt_zero continuousAt_zero
continuous' 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid closedBall SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	continuous_of_continuousAt_zero continuousAt_zero'
continuousAt_zero 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ball SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	continuousAt_zero' Filter.mem_of_superset ball_subset_closedBall
continuousAt_zero' 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid closedBall SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	continuousAt_zero_of_forall' le_or_gt NormOneClass.norm_one NormedDivisionRing.to_normOneClass Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing one_mul LE.le.trans_lt lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono NormedField.exists_norm_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Filter.mem_of_superset smul_closedBall_zero set_smul_mem_nhds_zero_iff norm_pos_iff closedBall_mono LT.lt.le
continuousAt_zero_of_forall 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ball SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	continuousAt_zero_of_forall' Filter.mem_of_superset ball_subset_closedBall
continuousAt_zero_of_forall' 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid closedBall SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	ContinuousAt.eq_1 Filter.HasBasis.tendsto_right_iff Metric.nhds_basis_closedBall map_zero AddGroupSeminormClass.toZeroHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass closedBall_zero_eq_preimage_closedBall
continuous_iff 📖	mathematical	Real Real.instLT Real.instZero	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ball	—	Filter.Tendsto.eventually_lt_const instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.tendsto' map_zero AddGroupSeminormClass.toZeroHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass ball_zero_eq continuous
continuous_of_continuousAt_zero 📖	mathematical	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Continuous	—	UniformContinuous.continuous uniformContinuous_of_continuousAt_zero isUniformAddGroup_of_addCommGroup
continuous_of_forall 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ball SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	continuous_of_continuousAt_zero continuousAt_zero_of_forall
continuous_of_forall' 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid closedBall SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	continuous_of_continuousAt_zero continuousAt_zero_of_forall'
continuous_of_le 📖	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	—	continuous_of_forall Filter.mem_of_superset IsOpen.mem_nhds ball_zero_eq isOpen_lt OrderTopology.to_orderClosedTopology instOrderTopologyReal continuous_const mem_ball_self ball_antitone
convexOn 📖	mathematical	—	ConvexOn Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.univ DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction instFunLike	—	convex_univ SubadditiveHomClass.map_add_le_add AddGroupSeminormClass.toSubadditiveHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass SeminormClass.map_smul_eq_mul smul_one_smul norm_smul NormedSpace.toNormSMulClass NormOneClass.norm_one NormedDivisionRing.to_normOneClass mul_one Real.norm_of_nonneg
convex_ball 📖	mathematical	—	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction ball SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	—	Set.ext Set.preimage_univ Set.sep_univ mem_ball sub_eq_add_neg ConvexOn.convex_lt Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing ConvexOn.translate_left convexOn
convex_closedBall 📖	mathematical	—	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction closedBall SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	—	closedBall_eq_biInter_ball convex_iInter₂ convex_ball
exists_apply_eq_finset_sup 📖	mathematical	Finset.Nonempty	Finset Finset.instMembership DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Real instFunLike Finset.sup instSemilatticeSup instOrderBot	—	NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass Finset.exists_mem_eq_sup finset_sup_apply
ext 📖	—	DFunLike.coe Seminorm Real instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe Seminorm Real instFunLike	—	ext
finset_sup_apply 📖	mathematical	—	DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Real instFunLike Finset.sup instSemilatticeSup instOrderBot NNReal.toReal NNReal instSemilatticeSupNNReal NNReal.instOrderBot Real.instLE Real.instZero NonnegHomClass.apply_nonneg AddCommMonoid.toAddMonoid Real.instAddCommMonoid Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.linearOrder AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass	—	Finset.cons_induction_on NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass Finset.sup_empty coe_bot bot_eq_zero NNReal.instCanonicallyOrderedAdd Pi.zero_apply Nat.cast_zero IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing Finset.sup_cons coe_sup Pi.sup_apply NNReal.coe_max
finset_sup_apply_le 📖	mathematical	Real Real.instLE Real.instZero DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike	Finset.sup instSemilatticeSup instOrderBot	—	CanLift.prf NNReal.canLift NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass finset_sup_apply NNReal.coe_le_coe Finset.sup_le
finset_sup_apply_lt 📖	mathematical	Real Real.instLT Real.instZero DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike	Finset.sup instSemilatticeSup instOrderBot	—	CanLift.prf NNReal.canLift LT.lt.le NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass finset_sup_apply NNReal.coe_lt_coe Finset.sup_lt_iff NNReal.coe_pos
finset_sup_le_sum 📖	mathematical	—	Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder Finset.sup instSemilatticeSup instOrderBot Finset.sum instAddCommMonoid	—	Finset.sup_le_iff Finset.sum_eq_sum_diff_singleton_add le_add_iff_nonneg_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid instIsOrderedCancelAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT bot_le
finset_sup_smul 📖	mathematical	—	Finset.sup Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instSemilatticeSup instOrderBot NNReal Function.hasSMul instSMul Algebra.toSMul Real instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring CommSemiring.toSemiring IsScalarTower.left instSemiringNNReal NNReal.instMulActionOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace	—	ext IsScalarTower.left smul_apply NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass finset_sup_apply NNReal.mul_finset_sup
iSup_apply 📖	mathematical	BddAbove Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder Set.range	DFunLike.coe Real instFunLike iSup instSupSet Real.instSupSet	—	coe_iSup_eq iSup_apply
inf_apply 📖	mathematical	—	DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Real instFunLike instInf iInf Real.instInfSet Real.instAdd SubNegMonoid.toSub	—	—
instIsOrderedCancelAddMonoid 📖	mathematical	—	IsOrderedCancelAddMonoid Seminorm instAddCommMonoid instPartialOrder	—	Function.Injective.isOrderedCancelAddMonoid Pi.isOrderedAddCancelMonoid Real.instIsOrderedCancelAddMonoid coe_add
instIsScalarTowerOfReal 📖	mathematical	—	IsScalarTower Seminorm instSMul	—	ext smul_assoc
instSeminormClass 📖	mathematical	—	SeminormClass Seminorm instFunLike	—	AddGroupSeminorm.add_le' AddGroupSeminorm.map_zero' AddGroupSeminorm.neg' smul'
le_def 📖	mathematical	—	Seminorm Preorder.toLE PartialOrder.toPreorder instPartialOrder Real Real.instLE DFunLike.coe instFunLike	—	—
le_finset_sup_apply 📖	mathematical	Finset Finset.instMembership	Real Real.instLE DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike Finset.sup instSemilatticeSup instOrderBot	—	Finset.le_sup
lt_def 📖	mathematical	—	Seminorm Preorder.toLT PartialOrder.toPreorder instPartialOrder Preorder.toLE Real Real.instLT DFunLike.coe instFunLike	—	Pi.lt_def
mem_ball 📖	mathematical	—	Set Set.instMembership ball Real Real.instLT DFunLike.coe Seminorm AddCommGroup.toAddGroup instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—
mem_ball_self 📖	mathematical	Real Real.instLT Real.instZero	Set Set.instMembership ball	—	sub_self map_zero AddGroupSeminormClass.toZeroHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass
mem_ball_zero 📖	mathematical	—	Set Set.instMembership ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real Real.instLT DFunLike.coe Seminorm AddCommGroup.toAddGroup instFunLike	—	mem_ball sub_zero
mem_closedBall 📖	mathematical	—	Set Set.instMembership closedBall Real Real.instLE DFunLike.coe Seminorm AddCommGroup.toAddGroup instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—
mem_closedBall_self 📖	mathematical	Real Real.instLE Real.instZero	Set Set.instMembership closedBall	—	sub_self map_zero AddGroupSeminormClass.toZeroHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass
mem_closedBall_zero 📖	mathematical	—	Set Set.instMembership closedBall NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real Real.instLE DFunLike.coe Seminorm AddCommGroup.toAddGroup instFunLike	—	mem_closedBall sub_zero
neg_ball 📖	mathematical	—	Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ball SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	Set.ext Set.mem_neg mem_ball neg_add' sub_neg_eq_add AddGroupSeminormClass.map_neg_eq_map SeminormClass.toAddGroupSeminormClass instSeminormClass
neg_closedBall 📖	mathematical	—	Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid closedBall SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	Set.ext Set.mem_neg mem_closedBall neg_add' sub_neg_eq_add AddGroupSeminormClass.map_neg_eq_map SeminormClass.toAddGroupSeminormClass instSeminormClass
neg_mem_ball_zero 📖	mathematical	—	Set Set.instMembership ball SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NegZeroClass.toNeg	—	AddGroupSeminormClass.map_neg_eq_map SeminormClass.toAddGroupSeminormClass instSeminormClass
neg_mem_closedBall_zero 📖	mathematical	—	Set Set.instMembership closedBall SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NegZeroClass.toNeg	—	AddGroupSeminormClass.map_neg_eq_map SeminormClass.toAddGroupSeminormClass instSeminormClass
norm_sub_map_le_sub 📖	mathematical	—	Real Real.instLE Norm.norm Real.norm Real.instSub DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike SubNegMonoid.toSub	—	abs_sub_map_le_sub Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass
preimage_metric_ball 📖	mathematical	—	Set.preimage Real DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike Metric.ball Real.pseudoMetricSpace Real.instZero setOf Real.instLT	—	Set.ext Real.norm_of_nonneg NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass
preimage_metric_closedBall 📖	mathematical	—	Set.preimage Real DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike Metric.closedBall Real.pseudoMetricSpace Real.instZero setOf Real.instLE	—	Set.ext Real.norm_of_nonneg NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass
pullback_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instAddMonoid AddMonoidHom.instFunLike pullback comp	—	—
rescale_to_shell 📖	mathematical	Real Real.instLT Real.instOne Norm.norm NormedField.toNorm Real.instZero	DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instInv Real.instMul	—	rescale_to_shell_zpow
rescale_to_shell_zpow 📖	mathematical	Real Real.instLT Real.instOne Norm.norm NormedField.toNorm Real.instZero	DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instInv Real.instMul	—	div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass exists_mem_Ico_zpow Real.instArchimedean AddGroup.existsAddOfLE lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one norm_zpow LT.lt.trans zpow_ne_zero norm_pos_iff SeminormClass.map_smul_eq_mul zpow_neg norm_inv div_eq_inv_mul div_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono mul_comm div_le_iff₀ zpow_add₀ ne_of_gt zpow_one mul_inv_rev mul_assoc mul_inv_cancel₀ one_mul le_div_iff₀ zpow_pos Real.instZeroLEOneClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul inv_inv mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono norm_nonneg
restrictScalars_ball 📖	mathematical	—	ball SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing restrictScalars SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	—
restrictScalars_closedBall 📖	mathematical	—	closedBall SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing restrictScalars SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	—
sSup_apply 📖	mathematical	BddAbove Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe Real instFunLike SupSet.sSup instSupSet iSup Set.Elem Real.instSupSet Set Set.instMembership	—	coe_sSup_eq iSup_apply
sSup_empty 📖	mathematical	—	SupSet.sSup Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid instSupSet Set Set.instEmptyCollection Bot.bot OrderBot.toBot Preorder.toLE Ring.toSemiring SeminormedRing.toRing PartialOrder.toPreorder instPartialOrder instOrderBot	—	ext sSup_apply bddAbove_empty Real.iSup_of_isEmpty Set.instIsEmptyElemEmptyCollection
smul' 📖	mathematical	—	AddGroupSeminorm.toFun toAddGroupSeminorm Real Real.instMul Norm.norm SeminormedRing.toNorm	—	—
smul_apply 📖	mathematical	—	DFunLike.coe Seminorm Real instFunLike instSMul	—	—
smul_ball_preimage 📖	mathematical	—	Set.preimage SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid ball SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Real DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedField.toNorm	—	Set.ext Set.mem_preimage mem_ball lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing norm_pos_iff mul_comm SeminormClass.map_smul_eq_mul instSeminormClass smul_sub smul_inv_smul₀
smul_ball_zero 📖	mathematical	—	Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid ball SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real Real.instMul Norm.norm NormedField.toNorm	—	Set.ext Set.mem_smul_set_iff_inv_smul_mem₀ mem_ball_zero SeminormClass.map_smul_eq_mul instSeminormClass norm_inv div_eq_inv_mul div_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing norm_pos_iff mul_comm
smul_closedBall_preimage 📖	mathematical	—	Set.preimage SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid closedBall SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Real DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedField.toNorm	—	Set.ext Set.mem_preimage mem_closedBall le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing norm_pos_iff mul_comm SeminormClass.map_smul_eq_mul instSeminormClass smul_sub smul_inv_smul₀
smul_closedBall_subset 📖	mathematical	—	Set Set.instHasSubset Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid closedBall SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real Real.instMul Norm.norm NormedField.toNorm	—	mem_closedBall_zero SeminormClass.map_smul_eq_mul instSeminormClass mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg
smul_closedBall_zero 📖	mathematical	Real Real.instLT Real.instZero Norm.norm NormedField.toNorm	Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid closedBall SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instMul	—	subset_antisymm Set.instAntisymmSubset smul_closedBall_subset Set.mem_smul_set mem_closedBall_zero SeminormClass.map_smul_eq_mul instSeminormClass norm_inv inv_mul_le_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing smul_assoc IsScalarTower.left smul_eq_mul div_eq_mul_inv div_self norm_pos_iff one_smul
smul_comp 📖	mathematical	—	comp Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instSMul	—	ext
smul_inf 📖	mathematical	—	Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid instSMul instInf	—	ext smul_one_smul Real.mul_iInf_of_nonneg NNReal.coe_nonneg mul_add Distrib.leftDistribClass
smul_le_smul 📖	mathematical	Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder NNReal instPartialOrderNNReal	instSMul Algebra.toSMul Real instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring CommSemiring.toSemiring IsScalarTower.left instSemiringNNReal NNReal.instMulActionOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace	—	IsScalarTower.left mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass NNReal.coe_nonneg
smul_sup 📖	mathematical	—	Seminorm instSMul instSup	—	smul_one_smul mul_max_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing NNReal.coe_nonneg ext
sub_mem_ball 📖	mathematical	—	Set Set.instMembership ball SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	sub_sub
sub_mem_closedBall 📖	mathematical	—	Set Set.instMembership closedBall SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	sub_sub
sup_apply 📖	mathematical	—	DFunLike.coe Seminorm Real instFunLike instSup Real.instMax	—	—
uniformContinuous 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ball SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	UniformContinuous Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	uniformContinuous_of_continuousAt_zero continuousAt_zero
uniformContinuous' 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid closedBall SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	UniformContinuous Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	uniformContinuous_of_continuousAt_zero continuousAt_zero'
uniformContinuous_of_continuousAt_zero 📖	mathematical	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	UniformContinuous	—	map_zero AddGroupSeminormClass.toZeroHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass UniformContinuous.eq_1 uniformity_eq_comap_nhds_zero_swapped IsUniformAddGroup.isRightUniformAddGroup Metric.uniformity_eq_comap_nhds_zero Filter.tendsto_comap_iff tendsto_of_tendsto_of_tendsto_of_le_of_le instOrderTopologyReal tendsto_const_nhds Filter.Tendsto.comp Filter.tendsto_comap dist_nonneg norm_sub_map_le_sub
uniformContinuous_of_forall 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ball SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	UniformContinuous Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	uniformContinuous_of_continuousAt_zero continuousAt_zero_of_forall
uniformContinuous_of_forall' 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid closedBall SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	UniformContinuous Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Seminorm instFunLike	—	uniformContinuous_of_continuousAt_zero continuousAt_zero_of_forall'
uniformSpace_eq_of_hasBasis 📖	mathematical	Filter.HasBasis nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set Filter Filter.instMembership closedBall SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Real Real.instLT Real.instZero Set.instHasSubset ball	PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace AddGroupSeminorm.toSeminormedAddGroup toAddGroupSeminorm	—	IsUniformAddGroup.ext SeminormedAddCommGroup.to_isUniformAddGroup le_antisymm comap_norm_nhds_zero Filter.tendsto_iff_comap continuous' IsUniformAddGroup.to_topologicalAddGroup Continuous.tendsto' map_zero AddGroupSeminormClass.toZeroHomClass SeminormClass.toAddGroupSeminormClass instSeminormClass Filter.HasBasis.le_basis_iff NormedAddCommGroup.nhds_zero_basis_norm_lt
uniformity_eq_of_hasBasis 📖	mathematical	Filter.HasBasis nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set Filter Filter.instMembership closedBall SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Real Real.instLT Real.instZero Set.instHasSubset ball	uniformity iInf Filter.instInfSet Filter.principal setOf DFunLike.coe Seminorm instFunLike SubNegMonoid.toSub	—	uniformSpace_eq_of_hasBasis
vadd_ball 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction addGroupIsAddTorsor ball	—	Metric.vadd_ball NormedAddGroup.to_isIsometricVAdd_left
vadd_closedBall 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction addGroupIsAddTorsor closedBall	—	Metric.vadd_closedBall NormedAddGroup.to_isIsometricVAdd_left
zero_apply 📖	mathematical	—	DFunLike.coe Seminorm Real instFunLike instZero Real.instZero	—	—
zero_comp 📖	mathematical	—	comp Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instZero	—	ext
zero_or_exists_apply_eq_finset_sup 📖	mathematical	—	DFunLike.coe Seminorm AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Real instFunLike Finset.sup instSemilatticeSup instOrderBot Real.instZero Finset Finset.instMembership	—	Finset.eq_empty_or_nonempty exists_apply_eq_finset_sup

SeminormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_smul_eq_mul 📖	mathematical	—	DFunLike.coe Real Real.instMul Norm.norm SeminormedRing.toNorm	—	—
toAddGroupSeminormClass 📖	mathematical	—	AddGroupSeminormClass Real Real.instAddCommMonoid Real.partialOrder	—	—

(root)

Definitions

Name	Category	Theorems
Seminorm 📖	CompData	154 math math: SchwartzMap.norm_toLp_le_seminorm, Seminorm.instSeminormClass, Seminorm.isBounded_const, Seminorm.smul_sup, Seminorm.mem_ball_zero, LinearMap.coe_toSeminorm, WithSeminorms.image_isVonNBounded_iff_seminorm_bounded, Seminorm.le_finset_sup_apply, Seminorm.norm_sub_map_le_sub, SchwartzMap.norm_le_seminorm, ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm, Seminorm.bot_eq_zero, Seminorm.smul_comp, Seminorm.closedBall_zero', Seminorm.ball_sup, Seminorm.finset_sup_apply, SchwartzMap.seminorm_le_bound, WithSeminorms.mem_nhds_iff, Seminorm.ext_iff, Seminorm.uniformContinuous_of_forall, SeminormFamily.filter_eq_iInf, Seminorm.bddAbove_range_iff, Seminorm.smul_inf, Seminorm.continuous_of_forall', Seminorm.continuous', Seminorm.coe_le_coe, Seminorm.continuousAt_zero_of_forall', Seminorm.mem_closedBall_zero, Seminorm.lt_def, WithSeminorms.tendsto_nhds', Seminorm.pullback_apply, PiTensorProduct.projectiveSeminorm_apply, SeminormFamily.finset_sup_comp, ContDiffMapSupportedIn.seminorm_le_iff, Seminorm.closedBall_zero_eq_preimage_closedBall, Seminorm.ball_smul, Seminorm.convexOn, Seminorm.coe_restrictScalars, PiTensorProduct.projectiveSeminorm_tprod_le, WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm, Seminorm.ball_zero_eq_preimage_ball, Seminorm.rescale_to_shell_zpow, Seminorm.continuous, Seminorm.coe_smul, WithSeminorms.isVonNBounded_iff_seminorm_bddAbove, Seminorm.instIsScalarTowerOfReal, PiTensorProduct.injectiveSeminorm_le_projectiveSeminorm, Seminorm.comp_smul, SchwartzMap.norm_iteratedFDeriv_le_seminorm, SchwartzMap.seminorm_le_bound', Seminorm.comp_zero, Seminorm.coe_sup, Seminorm.coe_add, PiTensorProduct.norm_eval_le_injectiveSeminorm, Seminorm.add_comp, Seminorm.bddAbove_iff, Seminorm.continuousAt_zero', Seminorm.closedBall_finset_sup, Seminorm.ball_zero', WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup, WithSeminorms.tendsto_nhds, WithSeminorms.isOpen_iff_mem_balls, Seminorm.const_isBounded, Seminorm.preimage_metric_closedBall, Seminorm.sSup_empty, Seminorm.add_apply, PiTensorProduct.dualSeminorms_bounded, PiTensorProduct.injectiveSeminorm_apply, ContDiffMapSupportedIn.seminorm_le_iff_withOrder, Seminorm.exists_apply_eq_finset_sup, WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded, SchwartzMap.integral_pow_mul_iteratedFDeriv_le, Seminorm.uniformContinuous, Seminorm.closedBall_smul, Seminorm.coe_bot, Seminorm.continuous_iff, WithSeminorms.continuous_seminorm, Seminorm.le_def, Seminorm.comp_apply, SchwartzMap.le_seminorm, SchwartzMap.eLpNorm_le_seminorm, Seminorm.closedBall_sup, WithSeminorms.congr_equiv, ContDiffMapSupportedIn.norm_apply_le_seminorm, Seminorm.inf_apply, Seminorm.bddBelow_range_add, ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm_withOrder, ContDiffMapSupportedIn.seminorm_apply, WithSeminorms.tendsto_nhds_atTop, ContDiffMapSupportedIn.seminorm_eq_bot_of_gt, PolynormableSpace.withSeminorms', Seminorm.zero_or_exists_apply_eq_finset_sup, Seminorm.rescale_to_shell, Seminorm.continuousAt_zero_of_forall, SeminormFamily.withSeminorms_iff_nhds_eq_iInf, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, coe_normSeminorm, Seminorm.mem_ball, Seminorm.gauge_ball, Seminorm.coe_comp, PiTensorProduct.norm_eval_le_projectiveSeminorm, WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded, Seminorm.instIsOrderedCancelAddMonoid, Seminorm.finset_sup_smul, Seminorm.isBounded_sup, ContDiffMapSupportedIn.seminorm_postcompLM_le, Seminorm.closedBall_bot, Seminorm.smul_apply, Seminorm.coe_zero, LinearMap.toSeminorm_apply, Seminorm.closedBall_finset_sup', SchwartzMap.seminorm_apply, SchwartzMap.le_seminorm', Seminorm.coeFnAddMonoidHom_apply, Seminorm.preimage_metric_ball, Seminorm.uniformContinuous', Seminorm.sup_apply, LinearMap.mem_span_iff_bound, WithSeminorms.partial_sups, Seminorm.closedBall_zero_eq, LinearMap.toSeminormFamily_apply, Seminorm.ball_finset_sup_eq_iInter, Seminorm.zero_comp, Seminorm.ball_finset_sup, PiTensorProduct.injectiveSeminorm_tprod_le, Seminorm.mem_closedBall, gaugeSeminorm_lt_one_of_isOpen, PolynormableSpace.withSeminorms, Seminorm.comp_smul_apply, Seminorm.coe_lt_coe, WithSeminorms.isVonNBounded_iff_seminorm_bounded, SeminormFamily.basisSets_mem, SeminormFamily.basisSets_iff, Seminorm.continuous_of_forall, Seminorm.ball_zero_eq, Seminorm.coeFnAddMonoidHom_injective, Seminorm.ball_finset_sup', SchwartzMap.one_add_le_sup_seminorm_apply, Seminorm.continuous_iff_continuous_comp, Seminorm.uniformContinuous_of_forall', Seminorm.zero_apply, WithSeminorms.hasBasis_ball, Seminorm.finset_sup_le_sum, gaugeSeminorm_toFun, Seminorm.continuousAt_zero, Seminorm.closedBall_finset_sup_eq_iInter, Seminorm.comp_add_le, Seminorm.ball_bot, PiTensorProduct.injectiveSeminorm_def, WithSeminorms.hasBasis_zero_ball, ContDiffMapSupportedIn.norm_toBoundedContinuousFunction, SchwartzMap.norm_pow_mul_le_seminorm, Seminorm.uniformity_eq_of_hasBasis, WithSeminorms.finset_sups
SeminormClass 📖	CompData	4 math math: Seminorm.instSeminormClass, instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, MulAlgebraNormClass.toSeminormClass, AlgebraNormClass.toSeminormClass
normSeminorm 📖	CompOp	7 math math: ball_normSeminorm, PiTensorProduct.dualSeminorms_bounded, PiTensorProduct.injectiveSeminorm_apply, closedBall_normSeminorm, coe_normSeminorm, norm_withSeminorms, PiTensorProduct.injectiveSeminorm_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absorbent_ball 📖	mathematical	Real Real.instLT Norm.norm SeminormedAddCommGroup.toNorm	Absorbent PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace	—	ball_normSeminorm Seminorm.absorbent_ball
absorbent_ball_zero 📖	mathematical	Real Real.instLT Real.instZero	Absorbent PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	ball_normSeminorm Seminorm.absorbent_ball_zero
balanced_ball_zero 📖	mathematical	—	Balanced SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	ball_normSeminorm Seminorm.balanced_ball_zero
balanced_closedBall_zero 📖	mathematical	—	Balanced SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	closedBall_normSeminorm Seminorm.balanced_closedBall_zero
ball_normSeminorm 📖	mathematical	—	Seminorm.ball SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toModule normSeminorm Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace	—	Set.ext dist_eq_norm
closedBall_normSeminorm 📖	mathematical	—	Seminorm.closedBall SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toModule normSeminorm Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace	—	Set.ext dist_eq_norm
coe_normSeminorm 📖	mathematical	—	DFunLike.coe Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real Seminorm.instFunLike normSeminorm Norm.norm SeminormedAddCommGroup.toNorm	—	—
rescale_to_shell 📖	mathematical	Real Real.instLT Real.instOne Norm.norm NormedField.toNorm Real.instZero	NormedAddCommGroup.toNorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instInv Real.instMul	—	rescale_to_shell_semi_normed norm_ne_zero_iff
rescale_to_shell_semi_normed 📖	mathematical	Real Real.instLT Real.instOne Norm.norm NormedField.toNorm Real.instZero	SeminormedAddCommGroup.toNorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instInv Real.instMul	—	Seminorm.rescale_to_shell
rescale_to_shell_semi_normed_zpow 📖	mathematical	Real Real.instLT Real.instOne Norm.norm NormedField.toNorm Real.instZero	SeminormedAddCommGroup.toNorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instInv Real.instMul	—	Seminorm.rescale_to_shell_zpow
rescale_to_shell_zpow 📖	mathematical	Real Real.instLT Real.instOne Norm.norm NormedField.toNorm Real.instZero	NormedAddCommGroup.toNorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instInv Real.instMul	—	rescale_to_shell_semi_normed_zpow norm_ne_zero_iff

---

← Back to Index