NNNorm

📁 Source: Mathlib/Analysis/Normed/Operator/NNNorm.lean

Statistics

Metric	Count
Definitions	0
Theorems lipschitz, exists_lt_apply_of_lt_opNNNorm, exists_lt_apply_of_lt_opNorm, exists_mul_lt_apply_of_lt_opNNNorm, exists_mul_lt_of_lt_opNorm, exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm, isLeast_opNNNorm, le_opENorm, le_opNNNorm, lipschitz, lipschitz_apply, nndist_le_opNNNorm, nnnorm_def, opENorm_comp_le, opNNNorm_comp_le, opNNNorm_eq_of_bounds, opNNNorm_le_bound, opNNNorm_le_bound', opNNNorm_le_iff, opNNNorm_le_of_lipschitz, opNNNorm_le_of_unit_nnnorm, opNNNorm_subsingleton, sSup_sphere_eq_nnnorm, sSup_sphere_eq_norm, sSup_unitClosedBall_eq_nnnorm, sSup_unitClosedBall_eq_norm, sSup_unit_ball_eq_nnnorm, sSup_unit_ball_eq_norm	28
Total	28

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lipschitz 📖	mathematical	—	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup toContinuousLinearMap DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	ContinuousLinearMap.lipschitz

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lt_apply_of_lt_opNNNorm 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField	instOneNNReal DFunLike.coe funLike	—	exists_mul_lt_apply_of_lt_opNNNorm nnnorm_ne_zero_iff nnnorm_zero MulZeroClass.mul_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass LT.lt.ne' LE.le.trans_lt zero_le' NormedField.exists_lt_nnnorm_lt NNReal.lt_inv_iff_mul_lt mul_assoc mul_comm inv_ne_zero inv_inv nnnorm_smul NormedSpace.toNormSMulClass MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass div_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono NNReal.instIsStrictOrderedRing Ne.bot_lt div_eq_mul_inv RingHomIsometric.nnnorm_map
exists_lt_apply_of_lt_opNorm 📖	mathematical	Real Real.instLT Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule hasOpNorm DenselyNormedField.toNontriviallyNormedField	NormedAddCommGroup.toNorm Real.instOne SeminormedAddCommGroup.toNorm DFunLike.coe funLike	—	norm_zero Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass CanLift.prf NNReal.canLift not_lt exists_lt_apply_of_lt_opNNNorm
exists_mul_lt_apply_of_lt_opNNNorm 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal DFunLike.coe funLike	—	notMem_of_lt_csInf nnnorm_def OrderBot.bddBelow
exists_mul_lt_of_lt_opNorm 📖	mathematical	Real Real.instLE Real.instZero Real.instLT Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule hasOpNorm	Real.instMul SeminormedAddCommGroup.toNorm DFunLike.coe funLike	—	CanLift.prf NNReal.canLift exists_mul_lt_apply_of_lt_opNNNorm
exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField	instOneNNReal DFunLike.coe funLike	—	exists_lt_apply_of_lt_opNNNorm eq_zero_or_nnnorm_pos map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass nnnorm_zero NNReal.instCanonicallyOrderedAdd inv_one one_mul mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono NNReal.instIsStrictOrderedRing inv_strictAnti₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LE.le.trans_lt zero_le map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass nnnorm_smul NormedSpace.toNormSMulClass nnnorm_inv nnnorm_algebraMap' NormedDivisionRing.to_normOneClass nnnorm_norm inv_mul_cancel₀ LT.lt.ne' map_smulₛₗ RingHomIsometric.nnnorm_map
isLeast_opNNNorm 📖	mathematical	—	IsLeast NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal setOf NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup	—	isLeast_Ici
le_opENorm 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring toSeminormedAddCommGroup	—	le_opNNNorm
le_opNNNorm 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal toSeminormedAddCommGroup	—	le_opNorm
lipschitz 📖	mathematical	—	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup DFunLike.coe funLike	—	AddMonoidHomClass.lipschitz_of_bound_nnnorm DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass le_opNNNorm
lipschitz_apply 📖	mathematical	—	LipschitzWith ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule PseudoMetricSpace.toPseudoEMetricSpace toPseudoMetricSpace NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe funLike	—	lipschitzWith_iff_norm_sub_le LE.le.trans_eq SeminormedAddCommGroup.toIsTopologicalAddGroup le_opNorm mul_comm
nndist_le_opNNNorm 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNDist.nndist PseudoMetricSpace.toNNDist SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup	—	dist_le_opNorm
nnnorm_def 📖	mathematical	—	NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup InfSet.sInf NNReal ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder NNReal.instConditionallyCompleteLinearOrderBot setOf	—	NNReal.eq NNReal.coe_sInf coe_nnnorm norm_def NNReal.coe_image
opENorm_comp_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm comp Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	opNNNorm_comp_le
opNNNorm_comp_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup comp Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	opNorm_comp_le
opNNNorm_eq_of_bounds 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	toSeminormedAddCommGroup	—	opNorm_eq_of_bounds zero_le NNReal.instCanonicallyOrderedAdd Subtype.forall'
opNNNorm_le_bound 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	toSeminormedAddCommGroup	—	opNorm_le_bound zero_le NNReal.instCanonicallyOrderedAdd
opNNNorm_le_bound' 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	toSeminormedAddCommGroup	—	opNorm_le_bound' zero_le NNReal.instCanonicallyOrderedAdd NNReal.coe_ne_zero
opNNNorm_le_iff 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup DFunLike.coe funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	opNorm_le_iff
opNNNorm_le_of_lipschitz 📖	mathematical	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup	—	opNorm_le_of_lipschitz
opNNNorm_le_of_unit_nnnorm 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike	toSeminormedAddCommGroup	—	opNorm_le_of_unit_norm NNReal.coe_nonneg NNReal.coe_eq_one
opNNNorm_subsingleton 📖	mathematical	—	NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup NNReal instZeroNNReal	—	NNReal.eq opNorm_subsingleton
sSup_sphere_eq_nnnorm 📖	mathematical	—	SupSet.sSup NNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder NNReal.instConditionallyCompleteLinearOrderBot Set.image NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Metric.sphere NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instOne toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField	—	subsingleton_or_nontrivial Metric.sphere_eq_empty_of_subsingleton one_ne_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Set.image_empty csSup_empty bot_eq_zero' NNReal.instCanonicallyOrderedAdd opNNNorm_subsingleton csSup_eq_of_forall_le_of_forall_lt_exists_gt Set.Nonempty.image NormedSpace.sphere_nonempty EMetric.instNontrivialTopologyOfNontrivial zero_le_one Real.instZeroLEOneClass mul_one le_opNorm_of_le Eq.le mem_sphere_zero_iff_norm exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm sub_zero
sSup_sphere_eq_norm 📖	mathematical	—	SupSet.sSup Real Real.instSupSet Set.image Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Metric.sphere NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne hasOpNorm DenselyNormedField.toNontriviallyNormedField	—	NNReal.coe_sSup Set.image_image sSup_sphere_eq_nnnorm
sSup_unitClosedBall_eq_nnnorm 📖	mathematical	—	SupSet.sSup NNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder NNReal.instConditionallyCompleteLinearOrderBot Set.image NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Metric.closedBall NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instOne toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField	—	unit_le_opNorm mem_closedBall_zero_iff le_antisymm csSup_le Set.Nonempty.image Metric.nonempty_closedBall zero_le_one Real.instZeroLEOneClass sSup_unit_ball_eq_nnnorm csSup_le_csSup' Set.image_mono Metric.ball_subset_closedBall
sSup_unitClosedBall_eq_norm 📖	mathematical	—	SupSet.sSup Real Real.instSupSet Set.image Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Metric.closedBall NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne hasOpNorm DenselyNormedField.toNontriviallyNormedField	—	NNReal.coe_sSup Set.image_image sSup_unitClosedBall_eq_nnnorm
sSup_unit_ball_eq_nnnorm 📖	mathematical	—	SupSet.sSup NNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder NNReal.instConditionallyCompleteLinearOrderBot Set.image NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Metric.ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instOne toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField	—	csSup_eq_of_forall_le_of_forall_lt_exists_gt Set.Nonempty.image Metric.nonempty_ball zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing mul_one le_opNorm_of_le LT.lt.le mem_ball_zero_iff exists_lt_apply_of_lt_opNNNorm
sSup_unit_ball_eq_norm 📖	mathematical	—	SupSet.sSup Real Real.instSupSet Set.image Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Metric.ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne hasOpNorm DenselyNormedField.toNontriviallyNormedField	—	NNReal.coe_sSup Set.image_image sSup_unit_ball_eq_nnnorm

---

← Back to Index