Basic

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

Statistics

Metric	Count
Definitions evalAddNorm, evalMulNorm, induced, induced, induced, induced, induced, induced, toNNNorm, induced, induced, toNNNorm, normAddGroupNorm, normAddGroupSeminorm, normGroupNorm, normGroupSeminorm	16
Theorems of_forall_le_norm, of_forall_le_norm', norm, nnnorm_eq_zero, nnnorm_eq_zero', norm_eq_zero, norm_eq_zero', of_forall_nnnorm_eq_zero, of_forall_nnnorm_eq_zero', of_forall_norm_eq_zero, of_forall_norm_eq_zero', of_exists_nnnorm_ne_zero, of_exists_nnnorm_ne_zero', of_exists_norm_ne_zero, of_exists_norm_ne_zero', nhds_basis_norm_lt, nhds_zero_basis_norm_lt, tendsto_nhds_nhds, tendsto_nhds_zero, uniformity_basis_dist, nhds_basis_norm_lt, nhds_one_basis_norm_lt, tendsto_nhds_nhds, tendsto_nhds_one, uniformity_basis_dist, disjoint_nhds, disjoint_nhds_zero, disjoint_nhds, disjoint_nhds_one, abs_norm, abs_norm', abs_norm_sub_norm_le, abs_norm_sub_norm_le', add_mem_ball_add_iff, add_mem_ball_iff_norm, add_mem_closedBall_add_iff, add_mem_closedBall_iff_norm, ball_eq, ball_eq', ball_one_eq, ball_zero_eq, coe_comp_nnnorm, coe_comp_nnnorm', coe_nnnorm, coe_nnnorm', coe_normAddGroupSeminorm, coe_normGroupNorm, coe_normGroupSeminorm, dist_eq_norm, dist_eq_norm', dist_eq_norm_div, dist_eq_norm_div', dist_eq_norm_sub, dist_eq_norm_sub', dist_indicator, dist_inv, dist_le_norm_add_norm, dist_le_norm_add_norm', dist_mulIndicator, dist_neg, dist_norm_norm_le, dist_norm_norm_le', dist_one, dist_one_left, dist_one_right, dist_prod_prod_le, dist_prod_prod_le_of_le, dist_sum_sum_le, dist_sum_sum_le_of_le, dist_zero, dist_zero_left, dist_zero_right, edist_eq_enorm_div, edist_eq_enorm_sub, edist_indicator, edist_mulIndicator, edist_one_eq_enorm, edist_one_left, edist_one_right, edist_zero_eq_enorm, edist_zero_left, edist_zero_right, enorm'_eq_iff_norm_eq, enorm'_le_iff_norm_le, enorm_add_le, enorm_add_le_of_le, enorm_add₃_le, enorm_add₄_le, enorm_div_le, enorm_div_rev, enorm_eq_iff_norm_eq, enorm_eq_zero, enorm_eq_zero', enorm_inv', enorm_le_iff_norm_le, enorm_mul_le', enorm_mul_le_of_le', enorm_multisetProd_le, enorm_multisetSum_le, enorm_mul₃_le', enorm_mul₄_le', enorm_ne_zero, enorm_ne_zero', enorm_neg, enorm_one', enorm_pos, enorm_pos', enorm_prod_le, enorm_prod_le_of_le, enorm_sub_le, enorm_sub_rev, enorm_sum_le, enorm_sum_le_of_le, enorm_zero, eq_of_norm_div_eq_zero, eq_of_norm_div_le_zero, eq_of_norm_sub_eq_zero, eq_of_norm_sub_le_zero, eq_one_or_nnnorm_pos, eq_one_or_norm_pos, eq_zero_or_nnnorm_pos, eq_zero_or_norm_pos, exists_enorm_lt, exists_enorm_lt', exists_nnnorm_ne_zero, exists_nnnorm_ne_zero', exists_norm_ne_zero, exists_norm_ne_zero', hasCompactSupport_norm_iff, indiscreteTopology_iff_forall_nnnorm_eq_zero, indiscreteTopology_iff_forall_nnnorm_eq_zero', indiscreteTopology_iff_forall_norm_eq_zero, indiscreteTopology_iff_forall_norm_eq_zero', inseparable_one_iff_norm, inseparable_zero_iff_norm, mem_ball_iff_norm, mem_ball_iff_norm', mem_ball_iff_norm'', mem_ball_iff_norm''', mem_ball_one_iff, mem_ball_zero_iff, mem_closedBall_iff_norm, mem_closedBall_iff_norm', mem_closedBall_iff_norm'', mem_closedBall_iff_norm''', mem_closedBall_one_iff, mem_closedBall_zero_iff, mem_eball_one_iff, mem_eball_zero_iff, mem_emetric_ball_one_iff, mem_emetric_ball_zero_iff, mem_sphere_iff_norm, mem_sphere_iff_norm', mem_sphere_one_iff_norm, mem_sphere_zero_iff_norm, mul_mem_ball_iff_norm, mul_mem_ball_mul_iff, mul_mem_closedBall_iff_norm, mul_mem_closedBall_mul_iff, ne_one_of_mem_sphere, ne_one_of_mem_unit_sphere, ne_one_of_nnnorm_ne_zero, ne_one_of_norm_ne_zero, ne_zero_of_mem_sphere, ne_zero_of_mem_unit_sphere, ne_zero_of_nnnorm_ne_zero, ne_zero_of_norm_ne_zero, nndist_eq_nnnorm, nndist_eq_nnnorm_div, nndist_eq_nnnorm_sub, nndist_indicator, nndist_mulIndicator, nndist_nnnorm_nnnorm_le, nndist_nnnorm_nnnorm_le', nndist_one_left, nndist_one_right, nndist_zero_left, nndist_zero_right, nnnorm_abs_zsmul, nnnorm_add_eq_nnnorm_left, nnnorm_add_eq_nnnorm_right, nnnorm_add_le, nnnorm_div_eq_nnnorm_left, nnnorm_div_eq_nnnorm_right, nnnorm_div_le, nnnorm_eq_zero, nnnorm_eq_zero', nnnorm_inv', nnnorm_isUnit_zsmul, nnnorm_le_add_nnnorm_add, nnnorm_le_add_nnnorm_add', nnnorm_le_insert, nnnorm_le_insert', nnnorm_le_mul_nnnorm_add, nnnorm_le_mul_nnnorm_add', nnnorm_le_nnnorm_add_nnnorm_div, nnnorm_le_nnnorm_add_nnnorm_div', nnnorm_le_nnnorm_add_nnnorm_sub, nnnorm_le_nnnorm_add_nnnorm_sub', nnnorm_mul_eq_nnnorm_left, nnnorm_mul_eq_nnnorm_right, nnnorm_mul_le', nnnorm_multiset_prod_le, nnnorm_multiset_sum_le, nnnorm_natAbs_smul, nnnorm_ne_zero_iff, nnnorm_ne_zero_iff', nnnorm_neg, nnnorm_nsmul_le, nnnorm_one', nnnorm_pos, nnnorm_pos', nnnorm_pow_le_mul_norm, nnnorm_pow_natAbs, nnnorm_prod_le, nnnorm_prod_le_of_le, nnnorm_sub_eq_nnnorm_left, nnnorm_sub_eq_nnnorm_right, nnnorm_sub_le, nnnorm_sum_le, nnnorm_sum_le_of_le, nnnorm_units_zsmul, nnnorm_zero, nnnorm_zpow_abs, nnnorm_zpow_isUnit, nontrivialTopology_iff_exists_nnnorm_ne_zero, nontrivialTopology_iff_exists_nnnorm_ne_zero', nontrivialTopology_iff_exists_norm_ne_zero, nontrivialTopology_iff_exists_norm_ne_zero', norm_abs_zsmul, norm_add_eq_norm_left, norm_add_eq_norm_right, norm_add_le, norm_add_le_of_le, norm_add_sub_norm_sub_le_two_mul, norm_add_sub_norm_sub_le_two_mul_min, norm_add₃_le, norm_add₄_le, norm_div_eq_norm_left, norm_div_eq_norm_right, norm_div_eq_zero_iff, norm_div_le, norm_div_le_norm_div_add_norm_div, norm_div_le_of_le, norm_div_pos_iff, norm_div_rev, norm_div_sub_norm_div_le_norm_div, norm_eq_of_mem_sphere, norm_eq_of_mem_sphere', norm_eq_zero, norm_eq_zero', norm_inv', norm_isUnit_zsmul, norm_le_add_norm_add, norm_le_add_norm_add', norm_le_insert, norm_le_insert', norm_le_mul_norm_add, norm_le_mul_norm_add', norm_le_norm_add_const_of_dist_le, norm_le_norm_add_const_of_dist_le', norm_le_norm_add_norm_div, norm_le_norm_add_norm_div', norm_le_norm_add_norm_sub, norm_le_norm_add_norm_sub', norm_le_norm_div_add, norm_le_norm_sub_add, norm_le_of_mem_closedBall, norm_le_of_mem_closedBall', norm_le_zero_iff, norm_le_zero_iff', norm_lt_of_mem_ball, norm_lt_of_mem_ball', norm_mul_eq_norm_left, norm_mul_eq_norm_right, norm_mul_le', norm_mul_le_of_le', norm_mul_sub_norm_div_le_two_mul, norm_mul_sub_norm_div_le_two_mul_min, norm_multiset_prod_le, norm_multiset_sum_le, norm_mul₃_le', norm_mul₄_le', norm_natAbs_smul, norm_ne_zero_iff, norm_ne_zero_iff', norm_neg, norm_nonneg, norm_nonneg', norm_nsmul_le, norm_of_subsingleton, norm_of_subsingleton', norm_one', norm_pos_iff, norm_pos_iff', norm_pow_le_mul_norm, norm_pow_natAbs, norm_prod_le, norm_prod_le_of_le, norm_sub_eq_norm_left, norm_sub_eq_norm_right, norm_sub_eq_zero_iff, norm_sub_le, norm_sub_le_norm_add, norm_sub_le_norm_mul, norm_sub_le_norm_sub_add_norm_sub, norm_sub_le_of_le, norm_sub_norm_le, norm_sub_norm_le', norm_sub_pos_iff, norm_sub_rev, norm_sub_sub_norm_sub_le_norm_sub, norm_sum_le, norm_sum_le_of_le, norm_toNNReal, norm_toNNReal', norm_units_zsmul, norm_zero, norm_zpow_abs, norm_zpow_isUnit, nsmul_mem_ball, nsmul_mem_closedBall, ofReal_norm, ofReal_norm', ofReal_norm_eq_enorm, ofReal_norm_eq_enorm', pow_mem_ball, pow_mem_closedBall, preimage_add_ball, preimage_add_closedBall, preimage_add_sphere, preimage_mul_ball, preimage_mul_closedBall, preimage_mul_sphere, smul_ball'', smul_closedBall'', toReal_coe_nnnorm, toReal_coe_nnnorm', toReal_enorm, toReal_enorm', vadd_ball'', vadd_closedBall'', zero_lt_one_add_norm_sq, zero_lt_one_add_norm_sq'	344
Total	360

DiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_forall_le_norm 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedAddGroup.toNorm	DiscreteTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace	—	of_forall_le_dist dist_eq_norm_sub sub_ne_zero
of_forall_le_norm' 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedGroup.toNorm	DiscreteTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace	—	of_forall_le_dist dist_eq_norm_div div_ne_one

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm 📖	mathematical	HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NormedAddGroup.toAddGroup	Real Real.instZero Norm.norm NormedAddGroup.toNorm	—	hasCompactSupport_norm_iff

IndiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnnorm_eq_zero 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm NNReal instZeroNNReal	—	indiscreteTopology_iff_forall_nnnorm_eq_zero
nnnorm_eq_zero' 📖	mathematical	—	NNNorm.nnnorm SeminormedGroup.toNNNorm NNReal instZeroNNReal	—	indiscreteTopology_iff_forall_nnnorm_eq_zero'
norm_eq_zero 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm Real Real.instZero	—	indiscreteTopology_iff_forall_norm_eq_zero
norm_eq_zero' 📖	mathematical	—	Norm.norm SeminormedGroup.toNorm Real Real.instZero	—	indiscreteTopology_iff_forall_norm_eq_zero'
of_forall_nnnorm_eq_zero 📖	mathematical	NNNorm.nnnorm SeminormedAddGroup.toNNNorm NNReal instZeroNNReal	IndiscreteTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace	—	indiscreteTopology_iff_forall_nnnorm_eq_zero
of_forall_nnnorm_eq_zero' 📖	mathematical	NNNorm.nnnorm SeminormedGroup.toNNNorm NNReal instZeroNNReal	IndiscreteTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace	—	indiscreteTopology_iff_forall_nnnorm_eq_zero'
of_forall_norm_eq_zero 📖	mathematical	Norm.norm SeminormedAddGroup.toNorm Real Real.instZero	IndiscreteTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace	—	indiscreteTopology_iff_forall_norm_eq_zero
of_forall_norm_eq_zero' 📖	mathematical	Norm.norm SeminormedGroup.toNorm Real Real.instZero	IndiscreteTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace	—	indiscreteTopology_iff_forall_norm_eq_zero'

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalAddNorm 📖	CompOp	—
evalMulNorm 📖	CompOp	—

NontrivialTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_exists_nnnorm_ne_zero 📖	mathematical	—	NontrivialTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace	—	nontrivialTopology_iff_exists_nnnorm_ne_zero
of_exists_nnnorm_ne_zero' 📖	mathematical	—	NontrivialTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace	—	nontrivialTopology_iff_exists_nnnorm_ne_zero'
of_exists_norm_ne_zero 📖	mathematical	—	NontrivialTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace	—	nontrivialTopology_iff_exists_norm_ne_zero
of_exists_norm_ne_zero' 📖	mathematical	—	NontrivialTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace	—	nontrivialTopology_iff_exists_norm_ne_zero'

NormedAddCommGroup

Definitions

Name	Category	Theorems
induced 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nhds_basis_norm_lt 📖	mathematical	—	Filter.HasBasis Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace Real.instLT Real.instZero setOf Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	ball_eq Metric.nhds_basis_ball
nhds_zero_basis_norm_lt 📖	mathematical	—	Filter.HasBasis Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Real.instLT Real.instZero setOf Norm.norm SeminormedAddGroup.toNorm	—	sub_zero nhds_basis_norm_lt
tendsto_nhds_nhds 📖	mathematical	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace Real Real.instLT Real.instZero Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	Metric.tendsto_nhds_nhds dist_eq_norm_sub
tendsto_nhds_zero 📖	mathematical	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Filter.Eventually Real Real.instLT Norm.norm SeminormedAddGroup.toNorm	—	Metric.tendsto_nhds dist_zero_right
uniformity_basis_dist 📖	mathematical	—	Filter.HasBasis Real uniformity PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace Real.instLT Real.instZero setOf Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	dist_eq_norm_sub Metric.uniformity_basis_dist

NormedAddGroup

Definitions

Name	Category	Theorems
induced 📖	CompOp	—

NormedCommGroup

Definitions

Name	Category	Theorems
induced 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nhds_basis_norm_lt 📖	mathematical	—	Filter.HasBasis Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace Real.instLT Real.instZero setOf Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	Metric.nhds_basis_ball
nhds_one_basis_norm_lt 📖	mathematical	—	Filter.HasBasis Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Real.instLT Real.instZero setOf Norm.norm SeminormedGroup.toNorm	—	div_one nhds_basis_norm_lt
tendsto_nhds_nhds 📖	mathematical	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace Real Real.instLT Real.instZero Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	dist_eq_norm_div
tendsto_nhds_one 📖	mathematical	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Filter.Eventually Real Real.instLT Norm.norm SeminormedGroup.toNorm	—	Metric.tendsto_nhds dist_one_right
uniformity_basis_dist 📖	mathematical	—	Filter.HasBasis Real uniformity PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace Real.instLT Real.instZero setOf Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	dist_eq_norm_div Metric.uniformity_basis_dist

NormedGroup

Definitions

Name	Category	Theorems
induced 📖	CompOp	—

SeminormedAddCommGroup

Definitions

Name	Category	Theorems
induced 📖	CompOp	—

SeminormedAddGroup

Definitions

Name	Category	Theorems
induced 📖	CompOp	—
toNNNorm 📖	CompOp	526 math math: ContinuousLinearEquiv.antilipschitz, edist_eq_enorm_sub, nnnorm_inv, MeasureTheory.Lp.mul_meas_ge_le_pow_enorm', Matrix.frobenius_nnnorm_mul, Complex.nnnorm_exp_I_mul_ofReal, List.nnnorm_prod, IsStarNormal.spectralRadius_eq_nnnorm, IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum, Orthonormal.nnnorm_eq_one, eq_zero_or_nnnorm_pos, LinearIsometry.nnnorm_toContinuousLinearMap, nnnorm_le_insert', nnnorm_cfcₙ_nnreal_le_iff, enorm_mul, Real.nnnorm_deriv_mulExpNegMulSq_le_one, ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm, enorm_sub_le, WithLp.nnnorm_toLp_inr, OrthonormalBasis.nnnorm_eq_one, Matrix.cstar_nnnorm_def, parallelogram_law_with_nnnorm, ApproximatesLinearOn.lipschitz, pi_nnnorm_le_iff, WithLp.prod_nnnorm_ofLp, ContinuousAlternatingMap.opNNNorm_pi, nnnorm_norm', DoubleCentralizer.nnnorm_def', nnnorm_cfcₙ_lt_iff, ContinuousLinearMap.nnnorm_def, CFC.nnnorm_sqrt, List.nnnorm_prod_le', nnnorm_nsmul_le, Pi.nnnorm_single, edist_zero_left, IsGreatest.nnnorm_cfcₙ, nnnorm_sum_le, edist_zero_eq_enorm, MulOpposite.nnnorm_unop, enorm_norm', FormalMultilinearSeries.changeOriginSeries_summable_aux₃, ContinuousLinearMap.opNNNorm_le_iff, nnnorm_le_add_nnnorm_add, nndist_midpoint_right, NNReal.enorm_eq, WithLp.prod_nnnorm_eq_add, nndist_smul₀, Complex.nnnorm_ratCast, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum, nnnorm_le_nnnorm_add_nnnorm_sub, ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero, Matrix.nnnorm_lt_iff, NormedField.exists_lt_nnnorm_lt, Real.nnnorm_exp_I_mul_ofReal_sub_one_le, NormedField.exists_nnnorm_lt_one, DoubleCentralizer.nnnorm_snd, CStarAlgebra.mem_Icc_iff_nnnorm_le_one, nnnorm_le_insert, PiLp.nnnorm_eq_of_L2, MeasureTheory.MemLp.meas_ge_lt_top, nndist_right_lineMap, FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius, spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div, nnnorm_algebraMap_nnreal, NonUnitalStarAlgHom.nnnorm_apply_le, ContinuousLinearMap.sSup_sphere_eq_nnnorm, ContinuousAlternatingMap.le_opNNNorm, Complex.reCLM_nnnorm, Unitization.nnnorm_def, Matrix.linfty_opNNNorm_mulVec, nndist_left_lineMap, ediam_smul_le, ApproximatesLinearOn.norm_fderiv_sub_le, IsGreatest.nnnorm_cfc_nnreal, WithLp.nnnorm_seminormedAddCommGroupToProd, NormedField.exists_one_lt_enorm, MeasureTheory.uniformIntegrable_iff, MeasureTheory.AEStronglyMeasurable.nnnorm, Real.enorm_natCast, nnnorm_div, nnnorm_one, ContinuousLinearMap.opNNNorm_prod, spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul, FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum, nnnorm_mul_le, Matrix.frobenius_nnnorm_one, PiLp.nnnorm_toLp_one, NormedField.exists_nnnorm_lt, nnnorm_mul₃_le, enorm_neg, NormedField.exists_lt_enorm, Matrix.linfty_opNNNorm_eq_opNNNorm, InnerProductSpace.nnnorm_rankOne, pi_nnnorm_lt_iff, BoundedContinuousFunction.lintegral_nnnorm_le, antilipschitzWith_mul_right, enorm_sub_rev, UniformSpace.Completion.nnnorm_coe, nndist_smul_le, DoubleCentralizer.nnnorm_def, Quaternion.nnnorm_star, nnnorm_star, nnnorm_cfcₙ_nnreal_lt, nndist_inv_inv₀, CStarAlgebra.nnnorm_le_iff_of_nonneg, NNReal.natCast_natAbs, nnnorm_smul, List.nnnorm_prod_le, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, ContinuousMultilinearMap.nnnorm_constOfIsEmpty, RingHomIsometric.enorm_map, NormedField.denseRange_nnnorm, MeasureTheory.SimpleFunc.nnnorm_approxOn_le, eventually_nnnorm_sub_lt, ContinuousLinearMap.nnnorm_toSpanSingleton, Hamming.nnnorm_eq_hammingNorm, indiscreteTopology_iff_forall_nnnorm_eq_zero, EuclideanSpace.nnnorm_single, BoundedContinuousFunction.nnnorm_def, pi_nnnorm_const, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, infEDist_smul₀, PiLp.nnnorm_toLp_single, nnnorm_zpow_le_mul_norm, Matrix.linfty_opNNNorm_toMatrix, BoundedContinuousFunction.Lp_nnnorm_le, FormalMultilinearSeries.compAlongComposition_nnnorm, ContinuousLinearMap.lipschitz, IsGreatest.nnnorm_cfc, PiLp.nnnorm_toLp_const', selfAdjoint.nnnorm_pow_two_pow, Real.nnnorm_nnratCast, SemilinearMapClass.nnbound_of_continuous, MeasureTheory.Measure.hausdorffMeasure_smul₀, MeasureTheory.lintegral_nnnorm_condExpL2_le, Finset.nnnorm_prod_le', spectrum.gelfand_formula, nndist_vadd_left, LinearIsometryEquiv.nnnorm_map, nnnorm_natAbs, nnnorm_multiset_sum_le, Seminorm.comp_smul, IsGreatest.nnnorm_cfcₙ_nnreal, Matrix.l2_opNNNorm_mulVec, PiLp.nnnorm_apply_le, RCLike.nnnorm_nnratCast, TensorProduct.nnnorm_tmul, ContinuousWithinAt.nnnorm, MeasureTheory.lintegral_enorm_of_nonneg, FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le, nnnorm_algebraMap, nnnorm_pow, nnnorm_apply_le_nnnorm_cfcₙ, toReal_enorm, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le, ContinuousLinearMap.lipschitz_apply, nnnorm_pow_le, Filter.IsIncreasingApproximateUnit.eventually_nnnorm, Prod.nnnorm_def, MeasureTheory.tendsto_indicator_ge, Complex.ofRealCLM_nnnorm, MeasureTheory.MemLp.eLpNormEssSup_indicator_norm_ge_eq_zero, FormalMultilinearSeries.changeOrigin_radius, RCLike.nnnorm_ofNat, MeasureTheory.UniformIntegrable.spec', TensorProduct.nnnorm_map, WithLp.prod_nnnorm_eq_of_L2, Matrix.l2_opNNNorm_conjTranspose, FormalMultilinearSeries.radius_inv_eq_limsup, MeasureTheory.L2.integral_inner_eq_sq_eLpNorm, nndist_left_midpoint, spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius, WithLp.prod_nnnorm_eq_of_L1, Inseparable.nnnorm_eq_nnnorm, RingHomIsometric.nnnorm_map, IsSelfAdjoint.nnnorm_mul_self, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, enorm_le_iff_norm_le, ContinuousMap.nnnorm_lt_iff, IsUltrametricDist.nnnorm_add_eq_max_of_nnnorm_ne_nnnorm, Pi.enorm_single, MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le_of_meas, MeasureTheory.lintegral_ofReal_le_lintegral_enorm, ContinuousLinearMap.nnnorm_holder_apply_apply_le, infEdist_smul₀, NormedField.exists_enorm_lt, nnnorm_surjective, nndist_midpoint_left, DoubleCentralizer.nnnorm_fst, MeasureTheory.L1.nnnorm_integral_le, nnnorm_neg, Module.Basis.exists_opNNNorm_le, ContinuousLinearMap.isLeast_opNNNorm, ContinuousMap.nnnorm_smul_const, Matrix.nnnorm_replicateRow, BoundedContinuousFunction.nnnorm_const_eq, IsUltrametricDist.nnnorm_add_one_le_max_nnnorm_one, nndist_midpoint_midpoint_le', nndist_center_homothety, ContinuousLinearEquiv.lipschitz, NormedSpace.equicontinuous_TFAE, Matrix.l2_opNNNorm_mul, Pi.sum_nnnorm_apply_le_nnnorm, PiLp.nnnorm_eq_ciSup, Matrix.nnnorm_entry_le_entrywise_sup_nnnorm, nnnorm_cfc_le_iff, CStarAlgebra.nnnorm_le_one_iff_of_nonneg, Real.nnnorm_mul_toNNReal, ContinuousMap.nnnorm_lt_iff_of_nonempty, MulOpposite.nnnorm_op, nnnorm_isUnit_zsmul, nnnorm_le_pi_nnnorm, Real.ofReal_le_enorm, NormedField.exists_one_lt_nnnorm, nnnorm_indicator_eq_indicator_nnnorm, NumberField.canonicalEmbedding.nnnorm_eq, nnnorm_intCast_abs, NormedField.exists_enorm_lt_one, ProbabilityTheory.IdentDistrib.nnnorm, Real.nnnorm_two, ContinuousMultilinearMap.isLeast_opNNNorm, Real.toNNReal_mul_nnnorm, nndist_lineMap_right, edist_smul₀, Pi.norm_def, enorm_one, Matrix.l2_opNNNorm_def, nndist_eq_nnnorm_sub, Real.enorm_eq_ofReal_abs, nnnorm_cfcₙ_nnreal_lt_iff, CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le, WithLp.unitization_nnnorm_inr, nnnorm_cfc_nnreal_lt, WithLp.nnnorm_toLp_inl, NonUnitalStarAlgHom.nnnorm_map, MeasureTheory.L1.nnnorm_Integral_le_one, Units.nnnorm_pos, ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos, MeasureTheory.hausdorffMeasure_homothety_image, spectralNorm_smul, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius, nnnorm_cfc_nnreal_le, nnnorm_inner_le_nnnorm, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnnorm_quasispectrum, IsometricContinuousFunctionalCalculus.nnnorm_spectrum_le, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id, Measurable.nnnorm, nnnorm_cfc_nnreal_le_iff, Matrix.frobenius_nnnorm_replicateRow, Real.nnnorm_abs, IsPrimitiveRoot.nnnorm_eq_one, Complex.conjCLE_nnorm, Matrix.frobenius_nnnorm_replicateCol, PiLp.nnnorm_toLp, DoubleCentralizer.nnnorm_fst_eq_snd, Real.enorm_of_nonneg, nndist_vadd_right, ContinuousLinearMap.sSup_unit_ball_eq_nnnorm, Matrix.nnnorm_transpose, nnnorm_zero, Complex.nnnorm_ofNat, nnnorm_units_zsmul, nndist_eq_nnnorm_vsub, WithLp.nnnorm_fst_le, ContinuousMultilinearMap.opNNNorm_prod, Complex.nnnorm_nnratCast, MeasureTheory.nnnorm_indicatorConstLp_le, IsUltrametricDist.nnnorm_nsmul_le, Matrix.frobenius_nnnorm_diagonal, MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le, ContinuousOn.nnnorm, spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty, nnnorm_smul_le, ContinuousLinearMap.le_opNNNorm, range_nnnorm, MeasureTheory.hausdorffMeasure_smul_right_image, nnnorm_apply_le_nnnorm_cfc, BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm, IsometricContinuousFunctionalCalculus.spectrum_le, nnnorm_pow_le', MeasureTheory.MemLp.integral_indicator_norm_ge_le, IsSelfAdjoint.spectralRadius_eq_nnnorm, BoundedContinuousFunction.nnnorm_coe_le_nnnorm, ofReal_norm_eq_enorm, nnnorm_eq_zero, FormalMultilinearSeries.changeOriginSeries_summable_aux₁, Complex.enorm_exp_I_mul_ofReal, BoundedContinuousFunction.nnnorm_le, nndist_zero_right, Matrix.nnnorm_conjTranspose, PadicAlgCl.valuation_def, AntilipschitzWith.le_mul_nnnorm, SeparationQuotient.nnnorm_mk, nnnorm_cfcₙHom, ContinuousLinearMap.opNNNorm_mul, CFC.nnnorm_rpow, WithLp.prod_nnnorm_eq_sup, BoundedContinuousFunction.nnnorm_const_le, enorm_norm, nnnorm_norm, MeasureTheory.lpNorm_const_smul, nnnorm_fderiv_norm_rpow_le, HasStrictFDerivAt.approximates_deriv_on_open_nhds, TrivSqZeroExt.nnnorm_def, ContinuousMultilinearMap.nnnorm_ofSubsingleton, lipschitzWith_one_nnnorm, ContinuousAlternatingMap.isLeast_opNNNorm, RCLike.nnnorm_conj, apply_le_nnnorm_cfc_nnreal, WithLp.nnnorm_snd_le, uniformContinuous_nnnorm, nnnorm_algebraMap', Complex.nnnorm_natCast, Valued.integer.exists_nnnorm_lt_one, ContinuousLinearMap.nndist_le_opNNNorm, coe_nnnorm, Matrix.linfty_opNNNorm_mul, ContinuousMultilinearMap.opNNNorm_pi, MemHolder.nnHolderNorm_smul, instENormSMulClass, antilipschitzWith_mul_left, RCLike.nnnorm_two, ContinuousLinearMap.opNNNorm_mul_flip_apply, ContinuousAlternatingMap.nnnorm_toContinuousMultilinearMap, Isometry.nnnorm_map_of_map_zero, ContinuousMap.nnnorm_eq_iSup_nnnorm, ContinuousLinearMap.opNNNorm_comp_le, IsUltrametricDist.isUltrametricDist_iff_isNonarchimedean_nnnorm, FormalMultilinearSeries.changeOriginSeries_summable_aux₂, Real.nnnorm_of_nonneg, TrivSqZeroExt.nnnorm_inl, Real.nnnorm_ofNat, MeasureTheory.MemLp.meas_ge_lt_top', Matrix.linfty_opNNNorm_replicateCol, Real.toNNReal_eq_nnnorm_of_nonneg, TensorProduct.nnnorm_assoc, Int.nnnorm_coe_units, MeasureTheory.setLIntegral_nnnorm_condExpIndSMul_le, ediam_smul₀, PiLp.nnnorm_eq_of_L1, nnnorm_natAbs_smul, NonUnitalIsometricContinuousFunctionalCalculus.quasispectrum_le, Pi.nnnorm_def, Unitization.nnnorm_eq_sup, ContinuousLinearMap.nnnorm_smulRight_apply, MeasureTheory.StronglyMeasurable.nnnorm, ContinuousMultilinearMap.opNNNorm_le_iff, BoundedContinuousFunction.nnnorm_coeFn_eq, NNReal.nnnorm_eq, Complex.nnnorm_exp_ofReal_mul_I, DilationEquiv.smulTorsor_ratio, nnnorm_commutator_sub_one_le, WithLp.prod_nnnorm_toLp, AEMeasurable.nnnorm, edist_zero_right, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le, nnnorm_cfcₙ_le_iff, IsUltrametricDist.nnnorm_intCast_le_one, Continuous.nnnorm, continuous_nnnorm, MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_pos_le, nnnorm_cfc_lt_iff, spectrum.spectralRadius_le_nnnorm, FormalMultilinearSeries.summable_nnnorm_mul_pow, ContinuousLinearMap.opNNNorm_le_of_lipschitz, Int.abs_le_floor_nnreal_iff, AlternatingMap.measure_def, nnnormHom_apply, MeasureTheory.eLpNormEssSup_lt_top_iff_isBoundedUnder, Int.nnnorm_natCast, Complex.imCLM_nnnorm, Finset.nnnorm_sum_le_sup_nnnorm, MeasureTheory.UniformIntegrable.spec, RCLike.nnnorm_nnqsmul, nnnorm_commutator_units_sub_one_le, IsUltrametricDist.nnnorm_natCast_le_one, ContinuousLinearMap.opNNNorm_subsingleton, Real.nnnorm_natCast, Complex.nnnorm_intCast, enorm_smul_le, LinearIsometry.nnnorm_map, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id, nndist_indicator, StarAlgEquiv.nnnorm_map, nnnorm_cfc_nnreal_lt_iff, Real.enorm_abs, coe_comp_nnnorm, nnnorm_le_nnnorm_add_nnnorm_sub', Matrix.nnnorm_diagonal, ContinuousAlternatingMap.nnnorm_ofSubsingleton, TensorProduct.nnnorm_comm, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, mem_emetric_ball_zero_iff, nndist_eq_nnnorm, MeasureTheory.Lp.meas_ge_le_mul_pow_enorm, spectrum.le_nnnorm_of_mem, Matrix.l2_opNNNorm_diagonal, Int.toNat_add_toNat_neg_eq_nnnorm, spectrum.exists_nnnorm_eq_spectralRadius, TrivSqZeroExt.nnnorm_inr, NormedField.denselyOrdered_range_nnnorm, PiLp.nnnorm_eq_sum, nnnorm_abs_zsmul, MeasureTheory.lintegral_enorm_of_ae_nonneg, ofReal_norm, nnnorm_mul, nndist_homothety_center, MeasureTheory.lintegral_nnnorm_condExpIndSMul_le, Polynomial.cauchyBound_X_add_C, CStarAlgebra.inr_mem_Icc_iff_nnnorm_le, Matrix.nnnorm_def, MonotoneOn.nnnorm_cfc, ContinuousLinearMap.nnnorm_id, Matrix.frobenius_nnnorm_def, ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero, Matrix.nnnorm_le_iff, Real.nnnorm_rpow_of_nonneg, ContinuousLinearEquiv.nnnorm_symm_pos, Complex.nnnorm_I, pi_nnnorm_const_le, Finset.nnnorm_prod_le, EuclideanSpace.nnnorm_eq, RCLike.nnnorm_natCast, CStarRing.nnnorm_self_mul_star, ContinuousAt.nnnorm, ContinuousLinearMap.nnbound, Polynomial.cauchyBound_X_sub_C, nnnorm_tangentSpace_vectorSpace, nnnorm_cfcHom, nndist_nnnorm_nnnorm_le, nndist_zero_left, SemilinearIsometryClass.nnnorm_map, enorm_pow, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id_le, CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le, ContinuousAlternatingMap.nnnorm_constOfIsEmpty, ContinuousAlternatingMap.opNNNorm_le_iff, ContinuousMultilinearMap.nnnorm_smulRight, Real.enorm_eq_ofReal, nnnorm_prod, IndiscreteTopology.nnnorm_eq_zero, Matrix.l2_opNNNorm_conjTranspose_mul_self, enorm_eq_iff_norm_eq, TensorProduct.nndist_tmul_le, toReal_coe_nnnorm, PiLp.nnnorm_seminormedAddCommGroupToPi, NormedField.valuation_apply, IsUltrametricDist.nnnorm_sub_eq_max_of_nnnorm_sub_ne_nnnorm_sub, RCLike.nnnorm_nsmul, Matrix.linfty_opNNNorm_replicateRow, mem_eball_zero_iff, MeasureTheory.hausdorffMeasure_homothety_preimage, Complex.enorm_exp_ofReal_mul_I, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm, HolderWith.smul, nndist_right_midpoint, PiLp.nnnorm_toLp_const, IsUltrametricDist.isNonarchimedean_nnnorm, Filter.Tendsto.nnnorm, TensorProduct.nnnorm_lid, nnnorm_sub_le, norm_toNNReal, ContinuousMultilinearMap.le_opNNNorm, Matrix.frobenius_nnnorm_transpose, Complex.nnnorm_real, nnnorm_cfcₙ_nnreal_le, apply_le_nnnorm_cfcₙ_nnreal, PadicComplex.nnnorm_extends, enorm_inv, Complex.nnnorm_eq_one_of_pow_eq_one, nnnorm_zpow, nnnorm_add_le, spectrum.spectralRadius_le_pow_nnnorm_pow_one_div, nnnorm_map, eHolderNorm_smul, ContinuousAlternatingMap.opNNNorm_prod, lipschitzWith_smul, WithLp.unitization_nnnorm_def, edist_smul_le, nnnorm_le_add_nnnorm_add', MonotoneOn.nnnorm_cfcₙ, ContinuousLinearMap.opNNNorm_mul_apply, one_le_nnnorm_one, nndist_self_homothety, Matrix.linfty_opNNNorm_diagonal, edist_indicator, CFC.nnnorm_nnrpow, FormalMultilinearSeries.radius_eq_liminf, IsometricContinuousFunctionalCalculus.isGreatest_spectrum, Matrix.linfty_opNNNorm_def, CStarRing.nnnorm_star_mul_self, IsUltrametricDist.nnnorm_add_le_max, CStarAlgebra.nnnorm_le_natCast_iff_of_nonneg, nnnorm_pos, NormedField.exists_lt_nnnorm, Prod.nnnorm_mk, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, Matrix.frobenius_nnnorm_conjTranspose, nnnorm_zsmul_le, nndist_homothety_self, CStarAlgebra.nnnorm_mem_spectrum_of_nonneg, BoundedContinuousFunction.nndist_le_two_nnnorm, CStarAlgebra.le_nnnorm_of_mem_quasispectrum, IsUltrametricDist.nnnorm_zsmul_le, nndist_eq_nnnorm_vsub', NonUnitalIsometricContinuousFunctionalCalculus.nnnorm_quasispectrum_le, Matrix.linfty_opNorm_def, egauge_le_of_smul_mem_of_ne, NumberField.house_eq_sup', PiLp.nnnorm_ofLp, Real.enorm_ofReal_of_nonneg, Matrix.norm_eq_sup_sup_nnnorm, Polynomial.IsRoot.norm_lt_cauchyBound, HolderWith.smul_iff, MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_le, ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc, nndist_lineMap_left, IsUltrametricDist.nnnorm_tsum_le, Matrix.nnnorm_replicateCol, IsSelfAdjoint.nnnorm_pow_two_pow, Quaternion.nnnorm_coe, LipschitzWith.nnorm_le_mul, FormalMultilinearSeries.comp_summable_nnreal, Unitization.nnnorm_inr, measurable_nnnorm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_nhds 📖	mathematical	—	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace toPseudoMetricSpace Real Real.instLT Real.instZero Filter.Eventually Real.instLE Norm.norm toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid toAddGroup	—	Filter.HasBasis.disjoint_iff_left NormedAddCommGroup.nhds_basis_norm_lt not_lt Filter.eventually_iff
disjoint_nhds_zero 📖	mathematical	—	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid toAddGroup Real Real.instLT Real.instZero Filter.Eventually Real.instLE Norm.norm toNorm	—	sub_zero disjoint_nhds

SeminormedCommGroup

Definitions

Name	Category	Theorems
induced 📖	CompOp	—

SeminormedGroup

Definitions

Name	Category	Theorems
induced 📖	CompOp	—
toNNNorm 📖	CompOp	77 math math: nnnorm_le_nnnorm_add_nnnorm_div', pi_nnnorm_lt_iff', nnnorm_zpow_isUnit, enorm'_eq_iff_norm_eq, nnnorm_norm', Pi.norm_def', enorm_norm', nnnorm_le_mul_nnnorm_add, Isometry.nnnorm_map_of_map_one, IsUltrametricDist.nnnorm_pow_le, pi_nnnorm_const', SeparationQuotient.nnnorm_mk', nndist_eq_nnnorm_div, coe_nnnorm', ofReal_norm', eq_one_or_nnnorm_pos, toReal_enorm', nnnorm_le_mul_nnnorm_add', ofReal_norm_eq_enorm', nnnorm_zpow_le_mul_norm, indiscreteTopology_iff_forall_nnnorm_eq_zero', AntilipschitzWith.le_mul_nnnorm', enorm'_le_iff_norm_le, ContinuousWithinAt.nnnorm', nnnorm_inv', nnnorm_mul_le', nnnorm_pos', IsUltrametricDist.nnnorm_mul_le_max, nndist_one_left, mem_emetric_ball_one_iff, enorm_inv', edist_one_right, nnnorm_eq_zero', coe_comp_nnnorm', Pi.nnnorm_def', pi_nnnorm_le_iff', norm_toNNReal', edist_one_eq_enorm, nnnorm_zpow_abs, edist_eq_enorm_div, Pi.sum_nnnorm_apply_le_nnnorm', nnnorm_pow_le_mul_norm, mem_eball_one_iff, nndist_mulIndicator, pi_nnnorm_const_le', nnnorm_pow_natAbs, ContinuousOn.nnnorm', nnnorm_le_nnnorm_add_nnnorm_div, nndist_nnnorm_nnnorm_le', enorm_div_rev, LipschitzWith.nnorm_le_mul', Filter.Tendsto.nnnorm', enorm_div_le, nnnorm_one', Prod.nnnorm_mk', uniformContinuous_nnnorm', nnnorm_multiset_prod_le, IsUltrametricDist.nnnorm_tprod_le, IsUltrametricDist.nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div, Inseparable.nnnorm_eq_nnnorm', IsUltrametricDist.nnnorm_zpow_le, IndiscreteTopology.nnnorm_eq_zero', continuous_nnnorm', Finset.nnnorm_prod_le_sup_nnnorm, nnnorm_map', IsUltrametricDist.nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm, Prod.nnnorm_def', nnnorm_prod_le, lipschitzWith_one_nnnorm', edist_one_left, Continuous.nnnorm', toReal_coe_nnnorm', ContinuousAt.nnnorm', nnnorm_le_pi_nnnorm', nnnorm_div_le, nndist_one_right, edist_mulIndicator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_nhds 📖	mathematical	—	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace toPseudoMetricSpace Real Real.instLT Real.instZero Filter.Eventually Real.instLE Norm.norm toNorm DivInvMonoid.toDiv Group.toDivInvMonoid toGroup	—	Filter.HasBasis.disjoint_iff_left NormedCommGroup.nhds_basis_norm_lt
disjoint_nhds_one 📖	mathematical	—	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid toGroup Real Real.instLT Real.instZero Filter.Eventually Real.instLE Norm.norm toNorm	—	div_one disjoint_nhds

(root)

Definitions

Name	Category	Theorems
normAddGroupNorm 📖	CompOp	—
normAddGroupSeminorm 📖	CompOp	1 math math: coe_normAddGroupSeminorm
normGroupNorm 📖	CompOp	1 math math: coe_normGroupNorm
normGroupSeminorm 📖	CompOp	1 math math: coe_normGroupSeminorm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_norm 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup Norm.norm SeminormedAddGroup.toNorm	—	abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_nonneg
abs_norm' 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup Norm.norm SeminormedGroup.toNorm	—	abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_nonneg'
abs_norm_sub_norm_le 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup Real.instSub Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	dist_eq_norm_sub sub_zero abs_dist_sub_le
abs_norm_sub_norm_le' 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup Real.instSub Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	dist_eq_norm_div div_one abs_dist_sub_le
add_mem_ball_add_iff 📖	mathematical	—	Set Set.instMembership Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	Metric.mem_ball dist_eq_norm_sub add_sub_add_right_eq_sub
add_mem_ball_iff_norm 📖	mathematical	—	Set Set.instMembership Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real Real.instLT Norm.norm SeminormedAddCommGroup.toNorm	—	mem_ball_iff_norm add_sub_cancel_left
add_mem_closedBall_add_iff 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	Metric.mem_closedBall dist_eq_norm_sub add_sub_add_right_eq_sub
add_mem_closedBall_iff_norm 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm	—	mem_closedBall_iff_norm add_sub_cancel_left
ball_eq 📖	mathematical	—	Metric.ball SeminormedAddGroup.toPseudoMetricSpace setOf Real Real.instLT Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	Set.ext Metric.mem_ball dist_eq_norm_sub
ball_eq' 📖	mathematical	—	Metric.ball SeminormedGroup.toPseudoMetricSpace setOf Real Real.instLT Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	Set.ext dist_eq_norm_div
ball_one_eq 📖	mathematical	—	Metric.ball SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup setOf Real Real.instLT Norm.norm SeminormedGroup.toNorm	—	Set.ext dist_one_right
ball_zero_eq 📖	mathematical	—	Metric.ball SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup setOf Real Real.instLT Norm.norm SeminormedAddGroup.toNorm	—	Set.ext Metric.mem_ball dist_zero_right
coe_comp_nnnorm 📖	mathematical	—	NNReal Real NNReal.toReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Norm.norm SeminormedAddGroup.toNorm	—	—
coe_comp_nnnorm' 📖	mathematical	—	NNReal Real NNReal.toReal NNNorm.nnnorm SeminormedGroup.toNNNorm Norm.norm SeminormedGroup.toNorm	—	—
coe_nnnorm 📖	mathematical	—	NNReal.toReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Norm.norm SeminormedAddGroup.toNorm	—	—
coe_nnnorm' 📖	mathematical	—	NNReal.toReal NNNorm.nnnorm SeminormedGroup.toNNNorm Norm.norm SeminormedGroup.toNorm	—	—
coe_normAddGroupSeminorm 📖	mathematical	—	DFunLike.coe AddGroupSeminorm SeminormedAddGroup.toAddGroup Real AddGroupSeminorm.funLike normAddGroupSeminorm Norm.norm SeminormedAddGroup.toNorm	—	—
coe_normGroupNorm 📖	mathematical	—	DFunLike.coe GroupNorm NormedGroup.toGroup Real GroupNorm.funLike normGroupNorm Norm.norm NormedGroup.toNorm	—	—
coe_normGroupSeminorm 📖	mathematical	—	DFunLike.coe GroupSeminorm SeminormedGroup.toGroup Real GroupSeminorm.funLike normGroupSeminorm Norm.norm SeminormedGroup.toNorm	—	—
dist_eq_norm 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	dist_eq_norm_sub
dist_eq_norm' 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	dist_eq_norm_sub'
dist_eq_norm_div 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedGroup.toPseudoMetricSpace Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	SeminormedGroup.dist_eq
dist_eq_norm_div' 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedGroup.toPseudoMetricSpace Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	dist_comm dist_eq_norm_div
dist_eq_norm_sub 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	SeminormedAddGroup.dist_eq
dist_eq_norm_sub' 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	dist_comm dist_eq_norm_sub
dist_indicator 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Norm.norm SeminormedAddGroup.toNorm symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff	—	dist_eq_norm_sub Set.apply_indicator_symmDiff norm_neg
dist_inv 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedCommGroup.toPseudoMetricSpace InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid SeminormedCommGroup.toCommGroup	—	dist_eq_norm_div norm_inv' inv_div div_inv_eq_mul mul_comm
dist_le_norm_add_norm 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace Real.instAdd Norm.norm SeminormedAddGroup.toNorm	—	dist_eq_norm_sub norm_sub_le
dist_le_norm_add_norm' 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedGroup.toPseudoMetricSpace Real.instAdd Norm.norm SeminormedGroup.toNorm	—	dist_eq_norm_div norm_div_le
dist_mulIndicator 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedGroup.toPseudoMetricSpace Set.mulIndicator InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Norm.norm SeminormedGroup.toNorm symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff	—	dist_eq_norm_div Set.apply_mulIndicator_symmDiff norm_inv'
dist_neg 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	dist_eq_norm_sub norm_neg neg_sub sub_neg_eq_add add_comm
dist_norm_norm_le 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Real.pseudoMetricSpace Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	abs_norm_sub_norm_le
dist_norm_norm_le' 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Real.pseudoMetricSpace Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	abs_norm_sub_norm_le'
dist_one 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Norm.norm SeminormedGroup.toNorm	—	dist_one_left
dist_one_left 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Norm.norm SeminormedGroup.toNorm	—	dist_comm dist_one_right
dist_one_right 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Norm.norm SeminormedGroup.toNorm	—	dist_eq_norm_div div_one
dist_prod_prod_le 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedCommGroup.toPseudoMetricSpace Finset.prod CommGroup.toCommMonoid SeminormedCommGroup.toCommGroup Finset.sum Real.instAddCommMonoid	—	dist_prod_prod_le_of_le le_rfl
dist_prod_prod_le_of_le 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedCommGroup.toPseudoMetricSpace	Finset.prod CommGroup.toCommMonoid SeminormedCommGroup.toCommGroup Finset.sum Real.instAddCommMonoid	—	dist_eq_norm_div norm_prod_le_of_le
dist_sum_sum_le 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAddCommMonoid	—	dist_sum_sum_le_of_le le_rfl
dist_sum_sum_le_of_le 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace	Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAddCommMonoid	—	dist_eq_norm_sub Finset.sum_sub_distrib norm_sum_le_of_le
dist_zero 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Norm.norm SeminormedAddGroup.toNorm	—	dist_zero_left
dist_zero_left 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Norm.norm SeminormedAddGroup.toNorm	—	dist_comm dist_zero_right
dist_zero_right 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Norm.norm SeminormedAddGroup.toNorm	—	dist_eq_norm_sub sub_zero
edist_eq_enorm_div 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedGroup.toPseudoMetricSpace ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	edist_dist dist_eq_norm_div ofReal_norm_eq_enorm'
edist_eq_enorm_sub 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	edist_dist dist_eq_norm_sub ofReal_norm_eq_enorm
edist_indicator 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff	—	edist_nndist nndist_indicator
edist_mulIndicator 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedGroup.toPseudoMetricSpace Set.mulIndicator InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup ENNReal.ofNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff	—	edist_nndist nndist_mulIndicator
edist_one_eq_enorm 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm	—	edist_one_right
edist_one_left 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup ENNReal.ofNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm	—	edist_nndist nndist_one_left
edist_one_right 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm	—	edist_nndist nndist_one_right
edist_zero_eq_enorm 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm	—	edist_zero_right
edist_zero_left 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm	—	edist_nndist nndist_zero_left
edist_zero_right 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm	—	edist_nndist nndist_zero_right
enorm'_eq_iff_norm_eq 📖	mathematical	—	ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm Norm.norm SeminormedGroup.toNorm	—	Real.toNNReal_eq_toNNReal_iff norm_nonneg'
enorm'_le_iff_norm_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm Real Real.instLE Norm.norm SeminormedGroup.toNorm	—	ENNReal.ofReal_le_ofReal_iff norm_nonneg' ENNReal.ofReal_le_ofReal
enorm_add_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	ESeminormedAddMonoid.enorm_add_le
enorm_add_le_of_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	LE.le.trans enorm_add_le add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
enorm_add₃_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	enorm_add_le_of_le enorm_add_le le_rfl
enorm_add₄_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	enorm_add_le_of_le enorm_add₃_le le_rfl
enorm_div_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	nnnorm_div_le
enorm_div_rev 📖	mathematical	—	ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	edist_eq_enorm_div PseudoEMetricSpace.edist_comm
enorm_eq_iff_norm_eq 📖	mathematical	—	ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm Norm.norm SeminormedAddGroup.toNorm	—	ofReal_norm Real.toNNReal_eq_toNNReal_iff norm_nonneg
enorm_eq_zero 📖	mathematical	—	ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm ENormedAddMonoid.toESeminormedAddMonoid ENNReal instZeroENNReal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid	—	ENormedAddMonoid.enorm_eq_zero
enorm_eq_zero' 📖	mathematical	—	ENorm.enorm ContinuousENorm.toENorm ESeminormedMonoid.toContinuousENorm ENormedMonoid.toESeminormedMonoid ENNReal instZeroENNReal MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass ESeminormedMonoid.toMonoid	—	—
enorm_inv' 📖	mathematical	—	ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup	—	nnnorm_inv'
enorm_le_iff_norm_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm Real Real.instLE Norm.norm SeminormedAddGroup.toNorm	—	ofReal_norm ENNReal.ofReal_le_ofReal_iff norm_nonneg ENNReal.ofReal_le_ofReal
enorm_mul_le' 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedMonoid.toContinuousENorm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass ESeminormedMonoid.toMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	ESeminormedMonoid.enorm_mul_le
enorm_mul_le_of_le' 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedMonoid.toContinuousENorm	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass ESeminormedMonoid.toMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	LE.le.trans enorm_mul_le' add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
enorm_multisetProd_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedMonoid.toContinuousENorm ESeminormedCommMonoid.toESeminormedMonoid Multiset.prod ESeminormedCommMonoid.toCommMonoid Multiset.sum ENNReal.instAddCommMonoid Multiset.map	—	Multiset.apply_prod_le_sum_map IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid Eq.le enorm_one' enorm_mul_le'
enorm_multisetSum_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm ESeminormedAddCommMonoid.toESeminormedAddMonoid Multiset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENNReal.instAddCommMonoid Multiset.map	—	Multiset.le_sum_of_subadditive ENNReal.instIsOrderedAddMonoid Eq.le enorm_zero enorm_add_le
enorm_mul₃_le' 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedMonoid.toContinuousENorm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass ESeminormedMonoid.toMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	enorm_mul_le_of_le' enorm_mul_le' le_rfl
enorm_mul₄_le' 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedMonoid.toContinuousENorm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass ESeminormedMonoid.toMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	enorm_mul_le_of_le' enorm_mul₃_le' le_rfl
enorm_ne_zero 📖	—	—	—	—	Iff.ne enorm_eq_zero
enorm_ne_zero' 📖	—	—	—	—	Iff.ne enorm_eq_zero'
enorm_neg 📖	mathematical	—	ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup	—	nnnorm_neg
enorm_one' 📖	mathematical	—	ENorm.enorm ContinuousENorm.toENorm ESeminormedMonoid.toContinuousENorm MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass ESeminormedMonoid.toMonoid ENNReal instZeroENNReal	—	ESeminormedMonoid.enorm_zero
enorm_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm ENormedAddMonoid.toESeminormedAddMonoid	—	pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd enorm_ne_zero
enorm_pos' 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal ENorm.enorm ContinuousENorm.toENorm ESeminormedMonoid.toContinuousENorm ENormedMonoid.toESeminormedMonoid	—	pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd enorm_ne_zero'
enorm_prod_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedMonoid.toContinuousENorm ESeminormedCommMonoid.toESeminormedMonoid Finset.prod ESeminormedCommMonoid.toCommMonoid Finset.sum ENNReal.instAddCommMonoid	—	Finset.apply_prod_le_sum_apply IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid Eq.le enorm_one' enorm_mul_le'
enorm_prod_le_of_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedMonoid.toContinuousENorm ESeminormedCommMonoid.toESeminormedMonoid	Finset.prod ESeminormedCommMonoid.toCommMonoid Finset.sum ENNReal.instAddCommMonoid	—	LE.le.trans enorm_prod_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid
enorm_sub_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	ENNReal.coe_le_coe nnnorm_sub_le
enorm_sub_rev 📖	mathematical	—	ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	edist_eq_enorm_sub PseudoEMetricSpace.edist_comm
enorm_sum_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm ESeminormedAddCommMonoid.toESeminormedAddMonoid Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENNReal.instAddCommMonoid	—	Finset.le_sum_of_subadditive ENNReal.instIsOrderedAddMonoid Eq.le enorm_zero enorm_add_le
enorm_sum_le_of_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm ESeminormedAddCommMonoid.toESeminormedAddMonoid	Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENNReal.instAddCommMonoid	—	LE.le.trans enorm_sum_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid
enorm_zero 📖	mathematical	—	ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ENNReal instZeroENNReal	—	ESeminormedAddMonoid.enorm_zero
eq_of_norm_div_eq_zero 📖	—	Norm.norm NormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid NormedGroup.toGroup Real Real.instZero	—	—	norm_div_eq_zero_iff
eq_of_norm_div_le_zero 📖	—	Real Real.instLE Norm.norm NormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid NormedGroup.toGroup Real.instZero	—	—	div_eq_one norm_le_zero_iff'
eq_of_norm_sub_eq_zero 📖	—	Norm.norm NormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup Real Real.instZero	—	—	norm_sub_eq_zero_iff
eq_of_norm_sub_le_zero 📖	—	Real Real.instLE Norm.norm NormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup Real.instZero	—	—	sub_eq_zero norm_le_zero_iff
eq_one_or_nnnorm_pos 📖	mathematical	—	InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid NormedGroup.toGroup NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm NormedGroup.toSeminormedGroup	—	eq_one_or_norm_pos
eq_one_or_norm_pos 📖	mathematical	—	InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid NormedGroup.toGroup Real Real.instLT Real.instZero Norm.norm NormedGroup.toNorm	—	LE.le.eq_or_lt norm_nonneg'
eq_zero_or_nnnorm_pos 📖	mathematical	—	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NormedAddGroup.toAddGroup NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm NormedAddGroup.toSeminormedAddGroup	—	eq_zero_or_norm_pos
eq_zero_or_norm_pos 📖	mathematical	—	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NormedAddGroup.toAddGroup Real Real.instLT Real.instZero Norm.norm NormedAddGroup.toNorm	—	norm_pos_iff norm_eq_zero LE.le.eq_or_lt norm_nonneg
exists_enorm_lt 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm	—	Filter.Frequently.exists Filter.Frequently.and_eventually Filter.frequently_iff_neBot Filter.Tendsto.eventually_lt_const instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Ne.bot_lt Continuous.tendsto' ContinuousENorm.continuous_enorm enorm_zero
exists_enorm_lt' 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedMonoid.toContinuousENorm	—	Filter.Frequently.exists Filter.Frequently.and_eventually Filter.frequently_iff_neBot Filter.Tendsto.eventually_lt_const instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Ne.bot_lt Continuous.tendsto' ContinuousENorm.continuous_enorm enorm_one'
exists_nnnorm_ne_zero 📖	—	—	—	—	nontrivialTopology_iff_exists_nnnorm_ne_zero
exists_nnnorm_ne_zero' 📖	—	—	—	—	nontrivialTopology_iff_exists_nnnorm_ne_zero'
exists_norm_ne_zero 📖	—	—	—	—	nontrivialTopology_iff_exists_norm_ne_zero
exists_norm_ne_zero' 📖	—	—	—	—	nontrivialTopology_iff_exists_norm_ne_zero'
hasCompactSupport_norm_iff 📖	mathematical	—	HasCompactSupport Real Real.instZero Norm.norm NormedAddGroup.toNorm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NormedAddGroup.toAddGroup	—	hasCompactSupport_comp_left norm_eq_zero
indiscreteTopology_iff_forall_nnnorm_eq_zero 📖	mathematical	—	IndiscreteTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace NNNorm.nnnorm SeminormedAddGroup.toNNNorm NNReal instZeroNNReal	—	TopologicalSpace.not_nontrivial_iff Iff.not nontrivialTopology_iff_exists_nnnorm_ne_zero
indiscreteTopology_iff_forall_nnnorm_eq_zero' 📖	mathematical	—	IndiscreteTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace NNNorm.nnnorm SeminormedGroup.toNNNorm NNReal instZeroNNReal	—	Iff.not nontrivialTopology_iff_exists_nnnorm_ne_zero'
indiscreteTopology_iff_forall_norm_eq_zero 📖	mathematical	—	IndiscreteTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace Norm.norm SeminormedAddGroup.toNorm Real Real.instZero	—	TopologicalSpace.not_nontrivial_iff Iff.not nontrivialTopology_iff_exists_norm_ne_zero
indiscreteTopology_iff_forall_norm_eq_zero' 📖	mathematical	—	IndiscreteTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace Norm.norm SeminormedGroup.toNorm Real Real.instZero	—	Iff.not nontrivialTopology_iff_exists_norm_ne_zero'
inseparable_one_iff_norm 📖	mathematical	—	Inseparable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Norm.norm SeminormedGroup.toNorm Real Real.instZero	—	Metric.inseparable_iff dist_one_right
inseparable_zero_iff_norm 📖	mathematical	—	Inseparable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Norm.norm SeminormedAddGroup.toNorm Real Real.instZero	—	Metric.inseparable_iff dist_zero_right
mem_ball_iff_norm 📖	mathematical	—	Set Set.instMembership Metric.ball SeminormedAddGroup.toPseudoMetricSpace Real Real.instLT Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	Metric.mem_ball dist_eq_norm_sub
mem_ball_iff_norm' 📖	mathematical	—	Set Set.instMembership Metric.ball SeminormedAddGroup.toPseudoMetricSpace Real Real.instLT Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	Metric.mem_ball' dist_eq_norm_sub
mem_ball_iff_norm'' 📖	mathematical	—	Set Set.instMembership Metric.ball SeminormedGroup.toPseudoMetricSpace Real Real.instLT Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	Metric.mem_ball dist_eq_norm_div
mem_ball_iff_norm''' 📖	mathematical	—	Set Set.instMembership Metric.ball SeminormedGroup.toPseudoMetricSpace Real Real.instLT Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	Metric.mem_ball' dist_eq_norm_div
mem_ball_one_iff 📖	mathematical	—	Set Set.instMembership Metric.ball SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Real Real.instLT Norm.norm SeminormedGroup.toNorm	—	Metric.mem_ball dist_one_right
mem_ball_zero_iff 📖	mathematical	—	Set Set.instMembership Metric.ball SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Real Real.instLT Norm.norm SeminormedAddGroup.toNorm	—	Metric.mem_ball dist_zero_right
mem_closedBall_iff_norm 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedAddGroup.toPseudoMetricSpace Real Real.instLE Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	Metric.mem_closedBall dist_eq_norm_sub
mem_closedBall_iff_norm' 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedAddGroup.toPseudoMetricSpace Real Real.instLE Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	Metric.mem_closedBall' dist_eq_norm_sub
mem_closedBall_iff_norm'' 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedGroup.toPseudoMetricSpace Real Real.instLE Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	Metric.mem_closedBall dist_eq_norm_div
mem_closedBall_iff_norm''' 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedGroup.toPseudoMetricSpace Real Real.instLE Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	Metric.mem_closedBall' dist_eq_norm_div
mem_closedBall_one_iff 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Real Real.instLE Norm.norm SeminormedGroup.toNorm	—	Metric.mem_closedBall dist_one_right
mem_closedBall_zero_iff 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Real Real.instLE Norm.norm SeminormedAddGroup.toNorm	—	Metric.mem_closedBall dist_zero_right
mem_eball_one_iff 📖	mathematical	—	Set Set.instMembership Metric.eball PseudoMetricSpace.toPseudoEMetricSpace SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm	—	Metric.mem_eball edist_one_right
mem_eball_zero_iff 📖	mathematical	—	Set Set.instMembership Metric.eball PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm	—	Metric.mem_eball edist_zero_right
mem_emetric_ball_one_iff 📖	mathematical	—	Set Set.instMembership Metric.eball PseudoMetricSpace.toPseudoEMetricSpace SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm	—	mem_eball_one_iff
mem_emetric_ball_zero_iff 📖	mathematical	—	Set Set.instMembership Metric.eball PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm	—	mem_eball_zero_iff
mem_sphere_iff_norm 📖	mathematical	—	Set Set.instMembership Metric.sphere SeminormedAddGroup.toPseudoMetricSpace Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	Metric.mem_sphere dist_eq_norm_sub
mem_sphere_iff_norm' 📖	mathematical	—	Set Set.instMembership Metric.sphere SeminormedGroup.toPseudoMetricSpace Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	dist_eq_norm_div
mem_sphere_one_iff_norm 📖	mathematical	—	Set Set.instMembership Metric.sphere SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Norm.norm SeminormedGroup.toNorm	—	div_one
mem_sphere_zero_iff_norm 📖	mathematical	—	Set Set.instMembership Metric.sphere SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Norm.norm SeminormedAddGroup.toNorm	—	mem_sphere_iff_norm sub_zero
mul_mem_ball_iff_norm 📖	mathematical	—	Set Set.instMembership Metric.ball SeminormedCommGroup.toPseudoMetricSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup Real Real.instLT Norm.norm SeminormedCommGroup.toNorm	—	mem_ball_iff_norm'' mul_div_cancel_left
mul_mem_ball_mul_iff 📖	mathematical	—	Set Set.instMembership Metric.ball SeminormedCommGroup.toPseudoMetricSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup	—	dist_eq_norm_div mul_div_mul_right_eq_div
mul_mem_closedBall_iff_norm 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedCommGroup.toPseudoMetricSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup Real Real.instLE Norm.norm SeminormedCommGroup.toNorm	—	mem_closedBall_iff_norm'' mul_div_cancel_left
mul_mem_closedBall_mul_iff 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedCommGroup.toPseudoMetricSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup	—	dist_eq_norm_div mul_div_mul_right_eq_div
ne_one_of_mem_sphere 📖	—	—	—	—	ne_one_of_norm_ne_zero norm_eq_of_mem_sphere'
ne_one_of_mem_unit_sphere 📖	—	—	—	—	ne_one_of_mem_sphere one_ne_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
ne_one_of_nnnorm_ne_zero 📖	—	—	—	—	nnnorm_one'
ne_one_of_norm_ne_zero 📖	—	—	—	—	norm_one'
ne_zero_of_mem_sphere 📖	—	—	—	—	ne_zero_of_norm_ne_zero norm_eq_of_mem_sphere
ne_zero_of_mem_unit_sphere 📖	—	—	—	—	ne_zero_of_mem_sphere one_ne_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
ne_zero_of_nnnorm_ne_zero 📖	—	—	—	—	nnnorm_zero
ne_zero_of_norm_ne_zero 📖	—	—	—	—	norm_zero
nndist_eq_nnnorm 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist SeminormedAddGroup.toPseudoMetricSpace NNNorm.nnnorm SeminormedAddGroup.toNNNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	nndist_eq_nnnorm_sub
nndist_eq_nnnorm_div 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist SeminormedGroup.toPseudoMetricSpace NNNorm.nnnorm SeminormedGroup.toNNNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	NNReal.eq dist_eq_norm_div
nndist_eq_nnnorm_sub 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist SeminormedAddGroup.toPseudoMetricSpace NNNorm.nnnorm SeminormedAddGroup.toNNNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	NNReal.eq dist_eq_norm_sub
nndist_indicator 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist SeminormedAddGroup.toPseudoMetricSpace Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup NNNorm.nnnorm SeminormedAddGroup.toNNNorm symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff	—	NNReal.eq dist_indicator
nndist_mulIndicator 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist SeminormedGroup.toPseudoMetricSpace Set.mulIndicator InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup NNNorm.nnnorm SeminormedGroup.toNNNorm symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff	—	NNReal.eq dist_mulIndicator
nndist_nnnorm_nnnorm_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNDist.nndist PseudoMetricSpace.toNNDist instPseudoMetricSpaceNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	NNReal.coe_le_coe dist_norm_norm_le
nndist_nnnorm_nnnorm_le' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNDist.nndist PseudoMetricSpace.toNNDist instPseudoMetricSpaceNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	NNReal.coe_le_coe dist_norm_norm_le'
nndist_one_left 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup NNNorm.nnnorm SeminormedGroup.toNNNorm	—	nndist_eq_nnnorm_div one_div nnnorm_inv'
nndist_one_right 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup NNNorm.nnnorm SeminormedGroup.toNNNorm	—	nndist_eq_nnnorm_div div_one
nndist_zero_left 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup NNNorm.nnnorm SeminormedAddGroup.toNNNorm	—	nndist_eq_nnnorm_sub zero_sub nnnorm_neg
nndist_zero_right 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup NNNorm.nnnorm SeminormedAddGroup.toNNNorm	—	nndist_eq_nnnorm_sub sub_zero
nnnorm_abs_zsmul 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SubNegMonoid.toZSMul AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup abs instLatticeInt Int.instAddGroup	—	NNReal.eq norm_abs_zsmul
nnnorm_add_eq_nnnorm_left 📖	mathematical	NNNorm.nnnorm SeminormedAddGroup.toNNNorm NNReal instZeroNNReal	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	NNReal.eq norm_add_eq_norm_left
nnnorm_add_eq_nnnorm_right 📖	mathematical	NNNorm.nnnorm SeminormedAddGroup.toNNNorm NNReal instZeroNNReal	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	NNReal.eq norm_add_eq_norm_right
nnnorm_add_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	NNReal.coe_le_coe norm_add_le
nnnorm_div_eq_nnnorm_left 📖	mathematical	NNNorm.nnnorm SeminormedGroup.toNNNorm NNReal instZeroNNReal	DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	NNReal.eq norm_div_eq_norm_left
nnnorm_div_eq_nnnorm_right 📖	mathematical	NNNorm.nnnorm SeminormedGroup.toNNNorm NNReal instZeroNNReal	DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	NNReal.eq norm_div_eq_norm_right
nnnorm_div_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	NNReal.coe_le_coe norm_div_le
nnnorm_eq_zero 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm NormedAddGroup.toSeminormedAddGroup NNReal instZeroNNReal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NormedAddGroup.toAddGroup	—	NNReal.coe_eq_zero coe_nnnorm norm_eq_zero
nnnorm_eq_zero' 📖	mathematical	—	NNNorm.nnnorm SeminormedGroup.toNNNorm NormedGroup.toSeminormedGroup NNReal instZeroNNReal InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid NormedGroup.toGroup	—	NNReal.coe_eq_zero coe_nnnorm' norm_eq_zero'
nnnorm_inv' 📖	mathematical	—	NNNorm.nnnorm SeminormedGroup.toNNNorm InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup	—	NNReal.eq norm_inv'
nnnorm_isUnit_zsmul 📖	mathematical	IsUnit Int.instMonoid	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SubNegMonoid.toZSMul AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	NNReal.eq norm_isUnit_zsmul
nnnorm_le_add_nnnorm_add 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	norm_le_add_norm_add
nnnorm_le_add_nnnorm_add' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	norm_le_add_norm_add'
nnnorm_le_insert 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	nnnorm_le_nnnorm_add_nnnorm_sub
nnnorm_le_insert' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	nnnorm_le_nnnorm_add_nnnorm_sub'
nnnorm_le_mul_nnnorm_add 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup	—	norm_le_mul_norm_add
nnnorm_le_mul_nnnorm_add' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup	—	norm_le_mul_norm_add'
nnnorm_le_nnnorm_add_nnnorm_div 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	norm_le_norm_add_norm_div
nnnorm_le_nnnorm_add_nnnorm_div' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	norm_le_norm_add_norm_div'
nnnorm_le_nnnorm_add_nnnorm_sub 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	norm_le_norm_add_norm_sub
nnnorm_le_nnnorm_add_nnnorm_sub' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	norm_le_norm_add_norm_sub'
nnnorm_mul_eq_nnnorm_left 📖	mathematical	NNNorm.nnnorm SeminormedGroup.toNNNorm NNReal instZeroNNReal	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup	—	NNReal.eq norm_mul_eq_norm_left
nnnorm_mul_eq_nnnorm_right 📖	mathematical	NNNorm.nnnorm SeminormedGroup.toNNNorm NNReal instZeroNNReal	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup	—	NNReal.eq norm_mul_eq_norm_right
nnnorm_mul_le' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	NNReal.coe_le_coe norm_mul_le'
nnnorm_multiset_prod_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm SeminormedCommGroup.toSeminormedGroup Multiset.prod CommGroup.toCommMonoid SeminormedCommGroup.toCommGroup Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Multiset.map	—	NNReal.coe_le_coe NNReal.coe_multiset_sum Multiset.map_map norm_multiset_prod_le
nnnorm_multiset_sum_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Multiset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Multiset.map	—	NNReal.coe_le_coe NNReal.coe_multiset_sum Multiset.map_map norm_multiset_sum_le
nnnorm_natAbs_smul 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SubNegMonoid.toZSMul	—	NNReal.eq norm_natAbs_smul
nnnorm_ne_zero_iff 📖	—	—	—	—	Iff.not nnnorm_eq_zero
nnnorm_ne_zero_iff' 📖	—	—	—	—	Iff.not nnnorm_eq_zero'
nnnorm_neg 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup	—	NNReal.eq norm_neg
nnnorm_nsmul_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	NNReal.coe_le_coe NNReal.coe_natCast norm_nsmul_le
nnnorm_one' 📖	mathematical	—	NNNorm.nnnorm SeminormedGroup.toNNNorm InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup NNReal instZeroNNReal	—	NNReal.eq norm_one'
nnnorm_pos 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm NormedAddGroup.toSeminormedAddGroup	—	pos_iff_ne_zero NNReal.instCanonicallyOrderedAdd nnnorm_ne_zero_iff
nnnorm_pos' 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm NormedGroup.toSeminormedGroup	—	pos_iff_ne_zero NNReal.instCanonicallyOrderedAdd nnnorm_ne_zero_iff'
nnnorm_pow_le_mul_norm 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	NNReal.coe_natCast norm_pow_le_mul_norm
nnnorm_pow_natAbs 📖	mathematical	—	NNNorm.nnnorm SeminormedGroup.toNNNorm Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup DivInvMonoid.toZPow	—	NNReal.eq norm_pow_natAbs
nnnorm_prod_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm SeminormedCommGroup.toSeminormedGroup Finset.prod CommGroup.toCommMonoid SeminormedCommGroup.toCommGroup Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	NNReal.coe_le_coe NNReal.coe_sum Finset.sum_congr norm_prod_le
nnnorm_prod_le_of_le 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm SeminormedCommGroup.toSeminormedGroup	Finset.prod CommGroup.toCommMonoid SeminormedCommGroup.toCommGroup Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	LE.le.trans_eq norm_prod_le_of_le NNReal.coe_sum
nnnorm_sub_eq_nnnorm_left 📖	mathematical	NNNorm.nnnorm SeminormedAddGroup.toNNNorm NNReal instZeroNNReal	SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	NNReal.eq norm_sub_eq_norm_left
nnnorm_sub_eq_nnnorm_right 📖	mathematical	NNNorm.nnnorm SeminormedAddGroup.toNNNorm NNReal instZeroNNReal	SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	NNReal.eq norm_sub_eq_norm_right
nnnorm_sub_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	NNReal.coe_le_coe norm_sub_le
nnnorm_sum_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	NNReal.coe_le_coe NNReal.coe_sum Finset.sum_congr norm_sum_le
nnnorm_sum_le_of_le 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	LE.le.trans_eq norm_sum_le_of_le NNReal.coe_sum
nnnorm_units_zsmul 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	NNReal.eq norm_isUnit_zsmul Units.isUnit
nnnorm_zero 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup NNReal instZeroNNReal	—	NNReal.eq norm_zero
nnnorm_zpow_abs 📖	mathematical	—	NNNorm.nnnorm SeminormedGroup.toNNNorm DivInvMonoid.toZPow Group.toDivInvMonoid SeminormedGroup.toGroup abs instLatticeInt Int.instAddGroup	—	NNReal.eq norm_zpow_abs
nnnorm_zpow_isUnit 📖	mathematical	IsUnit Int.instMonoid	NNNorm.nnnorm SeminormedGroup.toNNNorm DivInvMonoid.toZPow Group.toDivInvMonoid SeminormedGroup.toGroup	—	NNReal.eq norm_zpow_isUnit
nontrivialTopology_iff_exists_nnnorm_ne_zero 📖	mathematical	—	NontrivialTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace	—	TopologicalSpace.nontrivial_iff_exists_not_inseparable Metric.inseparable_iff_nndist nndist_eq_nnnorm_sub sub_zero
nontrivialTopology_iff_exists_nnnorm_ne_zero' 📖	mathematical	—	NontrivialTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace	—	nndist_eq_nnnorm_div div_one
nontrivialTopology_iff_exists_norm_ne_zero 📖	mathematical	—	NontrivialTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace	—	nontrivialTopology_iff_exists_nnnorm_ne_zero NNReal.ne_iff
nontrivialTopology_iff_exists_norm_ne_zero' 📖	mathematical	—	NontrivialTopology UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace	—	—
norm_abs_zsmul 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toZSMul AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup abs instLatticeInt Int.instAddGroup	—	le_total abs_of_nonneg Int.instAddLeftMono abs_of_nonpos neg_zsmul norm_neg
norm_add_eq_norm_left 📖	mathematical	Norm.norm SeminormedAddGroup.toNorm Real Real.instZero	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	le_antisymm add_zero norm_add_le norm_le_add_norm_add
norm_add_eq_norm_right 📖	mathematical	Norm.norm SeminormedAddGroup.toNorm Real Real.instZero	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	le_antisymm zero_add norm_add_le add_zero norm_le_add_norm_add'
norm_add_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Real.instAdd	—	dist_eq_norm_sub sub_neg_eq_add sub_zero zero_add dist_triangle
norm_add_le_of_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Real.instAdd	—	LE.le.trans norm_add_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
norm_add_sub_norm_sub_le_two_mul 📖	mathematical	—	Real Real.instLE Real.instSub Norm.norm SeminormedAddGroup.toNorm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SubNegMonoid.toSub Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat two_mul tsub_le_iff_left AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_add_cancel add_assoc norm_add₃_le
norm_add_sub_norm_sub_le_two_mul_min 📖	mathematical	—	Real Real.instLE Real.instSub Norm.norm SeminormedAddCommGroup.toNorm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SubNegMonoid.toSub Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instMin	—	Nat.instAtLeastTwoHAddOfNat mul_min_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo le_min norm_sub_rev add_comm norm_add_sub_norm_sub_le_two_mul
norm_add₃_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Real.instAdd	—	norm_add_le_of_le norm_add_le le_rfl
norm_add₄_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Real.instAdd	—	norm_add_le_of_le norm_add₃_le le_rfl
norm_div_eq_norm_left 📖	mathematical	Norm.norm SeminormedGroup.toNorm Real Real.instZero	DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	le_antisymm add_zero norm_div_le sub_zero norm_sub_norm_le'
norm_div_eq_norm_right 📖	mathematical	Norm.norm SeminormedGroup.toNorm Real Real.instZero	DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	le_antisymm zero_add norm_div_le norm_div_rev sub_zero norm_sub_norm_le'
norm_div_eq_zero_iff 📖	mathematical	—	Norm.norm NormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid NormedGroup.toGroup Real Real.instZero	—	norm_eq_zero' div_eq_one
norm_div_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup Real.instAdd	—	dist_eq_norm_div div_one one_div norm_inv' dist_triangle
norm_div_le_norm_div_add_norm_div 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup Real.instAdd	—	dist_eq_norm_div dist_triangle
norm_div_le_of_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedGroup.toNorm	DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup Real.instAdd	—	LE.le.trans norm_div_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
norm_div_pos_iff 📖	mathematical	—	Real Real.instLT Real.instZero Norm.norm NormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid NormedGroup.toGroup	—	LE.le.lt_iff_ne norm_nonneg' Iff.not norm_div_eq_zero_iff
norm_div_rev 📖	mathematical	—	Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	dist_eq_norm_div dist_comm
norm_div_sub_norm_div_le_norm_div 📖	mathematical	—	Real Real.instLE Real.instSub Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	div_div_div_cancel_right norm_sub_norm_le'
norm_eq_of_mem_sphere 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm Set Set.instMembership Metric.sphere SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup	—	mem_sphere_zero_iff_norm
norm_eq_of_mem_sphere' 📖	mathematical	—	Norm.norm SeminormedGroup.toNorm Set Set.instMembership Metric.sphere SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup	—	mem_sphere_one_iff_norm
norm_eq_zero 📖	mathematical	—	Norm.norm NormedAddGroup.toNorm Real Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NormedAddGroup.toAddGroup	—	LE.le.ge_iff_eq' norm_nonneg norm_le_zero_iff
norm_eq_zero' 📖	mathematical	—	Norm.norm NormedGroup.toNorm Real Real.instZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid NormedGroup.toGroup	—	LE.le.ge_iff_eq' norm_nonneg' norm_le_zero_iff'
norm_inv' 📖	mathematical	—	Norm.norm SeminormedGroup.toNorm InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup	—	one_div div_one norm_div_rev
norm_isUnit_zsmul 📖	mathematical	IsUnit Int.instMonoid	Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toZSMul AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	norm_natAbs_smul Int.isUnit_iff_natAbs_eq one_nsmul
norm_le_add_norm_add 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Real.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	add_sub_cancel_right norm_sub_le
norm_le_add_norm_add' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Real.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	add_assoc neg_add_cancel zero_add norm_add_le norm_neg add_comm
norm_le_insert 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Real.instAdd SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	norm_le_norm_add_norm_sub
norm_le_insert' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Real.instAdd SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	norm_le_norm_add_norm_sub'
norm_le_mul_norm_add 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm Real.instAdd MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup	—	mul_div_cancel_right norm_div_le
norm_le_mul_norm_add' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm Real.instAdd MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup	—	mul_assoc inv_mul_cancel one_mul norm_mul_le' norm_inv' add_comm
norm_le_norm_add_const_of_dist_le 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace	Norm.norm SeminormedAddGroup.toNorm Real.instAdd	—	norm_le_of_mem_closedBall
norm_le_norm_add_const_of_dist_le' 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedGroup.toPseudoMetricSpace	Norm.norm SeminormedGroup.toNorm Real.instAdd	—	norm_le_of_mem_closedBall'
norm_le_norm_add_norm_div 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm Real.instAdd DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	norm_div_rev norm_le_norm_add_norm_div'
norm_le_norm_add_norm_div' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm Real.instAdd DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	add_comm LE.le.trans_eq' norm_mul_le' div_mul_cancel
norm_le_norm_add_norm_sub 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Real.instAdd SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	norm_sub_rev norm_le_norm_add_norm_sub'
norm_le_norm_add_norm_sub' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Real.instAdd SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	add_comm LE.le.trans_eq' norm_add_le sub_add_cancel
norm_le_norm_div_add 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm Real.instAdd DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	div_one norm_div_le_norm_div_add_norm_div
norm_le_norm_sub_add 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Real.instAdd SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	sub_zero norm_sub_le_norm_sub_add_norm_sub
norm_le_of_mem_closedBall 📖	mathematical	Set Set.instMembership Metric.closedBall SeminormedAddGroup.toPseudoMetricSpace	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Real.instAdd	—	LE.le.trans norm_le_norm_add_norm_sub' add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid dist_eq_norm_sub
norm_le_of_mem_closedBall' 📖	mathematical	Set Set.instMembership Metric.closedBall SeminormedGroup.toPseudoMetricSpace	Real Real.instLE Norm.norm SeminormedGroup.toNorm Real.instAdd	—	LE.le.trans norm_le_norm_add_norm_div' add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid dist_eq_norm_div
norm_le_zero_iff 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddGroup.toNorm Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NormedAddGroup.toAddGroup	—	dist_zero_right dist_le_zero
norm_le_zero_iff' 📖	mathematical	—	Real Real.instLE Norm.norm NormedGroup.toNorm Real.instZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid NormedGroup.toGroup	—	dist_one_right dist_le_zero
norm_lt_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.ball SeminormedAddGroup.toPseudoMetricSpace	Real Real.instLT Norm.norm SeminormedAddGroup.toNorm Real.instAdd	—	LE.le.trans_lt norm_le_norm_add_norm_sub' add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid dist_eq_norm_sub
norm_lt_of_mem_ball' 📖	mathematical	Set Set.instMembership Metric.ball SeminormedGroup.toPseudoMetricSpace	Real Real.instLT Norm.norm SeminormedGroup.toNorm Real.instAdd	—	LE.le.trans_lt norm_le_norm_add_norm_div' add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid dist_eq_norm_div
norm_mul_eq_norm_left 📖	mathematical	Norm.norm SeminormedGroup.toNorm Real Real.instZero	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup	—	le_antisymm add_zero norm_mul_le' norm_le_mul_norm_add
norm_mul_eq_norm_right 📖	mathematical	Norm.norm SeminormedGroup.toNorm Real Real.instZero	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup	—	le_antisymm zero_add norm_mul_le' add_zero norm_le_mul_norm_add'
norm_mul_le' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup Real.instAdd	—	dist_eq_norm_div div_inv_eq_mul div_one one_mul dist_triangle
norm_mul_le_of_le' 📖	mathematical	Real Real.instLE Norm.norm SeminormedGroup.toNorm	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup Real.instAdd	—	LE.le.trans norm_mul_le' add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
norm_mul_sub_norm_div_le_two_mul 📖	mathematical	—	Real Real.instLE Real.instSub Norm.norm SeminormedGroup.toNorm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup DivInvMonoid.toDiv Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat two_mul AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_mul_cancel add_assoc norm_mul₃_le'
norm_mul_sub_norm_div_le_two_mul_min 📖	mathematical	—	Real Real.instLE Real.instSub Norm.norm SeminormedCommGroup.toNorm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup DivInvMonoid.toDiv Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instMin	—	Nat.instAtLeastTwoHAddOfNat mul_min_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo le_min norm_div_rev mul_comm norm_mul_sub_norm_div_le_two_mul
norm_multiset_prod_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedCommGroup.toNorm Multiset.prod CommGroup.toCommMonoid SeminormedCommGroup.toCommGroup Multiset.sum Real.instAddCommMonoid Multiset.map	—	Multiset.apply_prod_le_sum_map IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Eq.le norm_one' norm_mul_le'
norm_multiset_sum_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Multiset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAddCommMonoid Multiset.map	—	Multiset.le_sum_of_subadditive Real.instIsOrderedAddMonoid Eq.le norm_zero norm_add_le
norm_mul₃_le' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup Real.instAdd	—	norm_mul_le_of_le' norm_mul_le' le_rfl
norm_mul₄_le' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup Real.instAdd	—	norm_mul_le_of_le' norm_mul₃_le' le_rfl
norm_natAbs_smul 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SubNegMonoid.toZSMul	—	natCast_zsmul Int.abs_eq_natAbs norm_abs_zsmul
norm_ne_zero_iff 📖	—	—	—	—	Iff.not norm_eq_zero
norm_ne_zero_iff' 📖	—	—	—	—	Iff.not norm_eq_zero'
norm_neg 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup	—	zero_sub sub_zero norm_sub_rev
norm_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero Norm.norm SeminormedAddGroup.toNorm	—	dist_zero_right dist_nonneg
norm_nonneg' 📖	mathematical	—	Real Real.instLE Real.instZero Norm.norm SeminormedGroup.toNorm	—	dist_one_right dist_nonneg
norm_nsmul_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Real.instMul Real.instNatCast	—	zero_nsmul norm_zero Nat.cast_zero MulZeroClass.zero_mul le_refl succ_nsmul Nat.cast_add Nat.cast_one add_mul Distrib.rightDistribClass one_mul norm_add_le_of_le le_rfl
norm_of_subsingleton 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm Real Real.instZero	—	norm_zero
norm_of_subsingleton' 📖	mathematical	—	Norm.norm SeminormedGroup.toNorm Real Real.instZero	—	norm_one'
norm_one' 📖	mathematical	—	Norm.norm SeminormedGroup.toNorm InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Real Real.instZero	—	dist_one_right dist_self
norm_pos_iff 📖	mathematical	—	Real Real.instLT Real.instZero Norm.norm NormedAddGroup.toNorm	—	not_le norm_le_zero_iff
norm_pos_iff' 📖	mathematical	—	Real Real.instLT Real.instZero Norm.norm NormedGroup.toNorm	—	not_le norm_le_zero_iff'
norm_pow_le_mul_norm 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup Real.instMul Real.instNatCast	—	pow_zero norm_one' Nat.cast_zero MulZeroClass.zero_mul pow_succ Nat.cast_add Nat.cast_one add_mul Distrib.rightDistribClass one_mul norm_mul_le_of_le' le_rfl
norm_pow_natAbs 📖	mathematical	—	Norm.norm SeminormedGroup.toNorm Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup DivInvMonoid.toZPow	—	zpow_natCast Int.abs_eq_natAbs norm_zpow_abs
norm_prod_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedCommGroup.toNorm Finset.prod CommGroup.toCommMonoid SeminormedCommGroup.toCommGroup Finset.sum Real.instAddCommMonoid	—	Finset.apply_prod_le_sum_apply IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Eq.le norm_one' norm_mul_le'
norm_prod_le_of_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedCommGroup.toNorm	Finset.prod CommGroup.toCommMonoid SeminormedCommGroup.toCommGroup Finset.sum Real.instAddCommMonoid	—	LE.le.trans norm_prod_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
norm_sub_eq_norm_left 📖	mathematical	Norm.norm SeminormedAddGroup.toNorm Real Real.instZero	SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	le_antisymm add_zero norm_sub_le sub_zero norm_sub_norm_le
norm_sub_eq_norm_right 📖	mathematical	Norm.norm SeminormedAddGroup.toNorm Real Real.instZero	SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	le_antisymm zero_add norm_sub_le norm_sub_rev sub_zero norm_sub_norm_le
norm_sub_eq_zero_iff 📖	mathematical	—	Norm.norm NormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup Real Real.instZero	—	norm_eq_zero sub_eq_zero
norm_sub_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Real.instAdd	—	dist_eq_norm_sub sub_zero zero_sub norm_neg dist_triangle
norm_sub_le_norm_add 📖	mathematical	—	Real Real.instLE Real.instSub Norm.norm SeminormedAddGroup.toNorm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	tsub_le_iff_right AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_neg_cancel_right norm_neg norm_add_le
norm_sub_le_norm_mul 📖	mathematical	—	Real Real.instLE Real.instSub Norm.norm SeminormedGroup.toNorm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup	—	AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_inv_cancel_right norm_inv' norm_mul_le'
norm_sub_le_norm_sub_add_norm_sub 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Real.instAdd	—	dist_eq_norm_sub dist_triangle
norm_sub_le_of_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm	SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Real.instAdd	—	LE.le.trans norm_sub_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
norm_sub_norm_le 📖	mathematical	—	Real Real.instLE Real.instSub Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	LE.le.trans le_abs_self abs_norm_sub_norm_le
norm_sub_norm_le' 📖	mathematical	—	Real Real.instLE Real.instSub Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	LE.le.trans le_abs_self abs_norm_sub_norm_le'
norm_sub_pos_iff 📖	mathematical	—	Real Real.instLT Real.instZero Norm.norm NormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup	—	LE.le.lt_iff_ne norm_nonneg Iff.not norm_sub_eq_zero_iff
norm_sub_rev 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	dist_eq_norm_sub dist_comm
norm_sub_sub_norm_sub_le_norm_sub 📖	mathematical	—	Real Real.instLE Real.instSub Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	sub_sub_sub_cancel_right norm_sub_norm_le
norm_sum_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAddCommMonoid	—	Finset.le_sum_of_subadditive Real.instIsOrderedAddMonoid Eq.le norm_zero norm_add_le
norm_sum_le_of_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm	Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAddCommMonoid	—	LE.le.trans norm_sum_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
norm_toNNReal 📖	mathematical	—	Real.toNNReal Norm.norm SeminormedAddGroup.toNorm NNNorm.nnnorm SeminormedAddGroup.toNNNorm	—	Real.toNNReal_coe
norm_toNNReal' 📖	mathematical	—	Real.toNNReal Norm.norm SeminormedGroup.toNorm NNNorm.nnnorm SeminormedGroup.toNNNorm	—	Real.toNNReal_coe
norm_units_zsmul 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	norm_isUnit_zsmul Units.isUnit
norm_zero 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Real Real.instZero	—	dist_zero_right dist_self
norm_zpow_abs 📖	mathematical	—	Norm.norm SeminormedGroup.toNorm DivInvMonoid.toZPow Group.toDivInvMonoid SeminormedGroup.toGroup abs instLatticeInt Int.instAddGroup	—	le_total abs_of_nonneg Int.instAddLeftMono abs_of_nonpos zpow_neg norm_inv'
norm_zpow_isUnit 📖	mathematical	IsUnit Int.instMonoid	Norm.norm SeminormedGroup.toNorm DivInvMonoid.toZPow Group.toDivInvMonoid SeminormedGroup.toGroup	—	norm_pow_natAbs Int.isUnit_iff_natAbs_eq pow_one
nsmul_mem_ball 📖	mathematical	Set Set.instMembership Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace	AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real Real.instAddMonoid	—	Metric.mem_ball dist_eq_norm_sub nsmul_sub lt_of_le_of_lt norm_nsmul_le Nat.cast_zero Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing nsmul_eq_mul lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.without_one_mul CancelDenoms.sub_subst CancelDenoms.mul_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le
nsmul_mem_closedBall 📖	mathematical	Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace	AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real Real.instAddMonoid	—	Metric.mem_closedBall dist_eq_norm_sub nsmul_sub LE.le.trans norm_nsmul_le nsmul_eq_mul mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing Nat.cast_nonneg
ofReal_norm 📖	mathematical	—	ENNReal.ofReal Norm.norm SeminormedAddGroup.toNorm ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm	—	norm_nonneg sup_of_le_left
ofReal_norm' 📖	mathematical	—	ENNReal.ofReal Norm.norm SeminormedGroup.toNorm ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm	—	norm_nonneg' sup_of_le_left
ofReal_norm_eq_enorm 📖	mathematical	—	ENNReal.ofReal Norm.norm SeminormedAddGroup.toNorm ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm	—	ENNReal.ofReal_eq_coe_nnreal norm_nonneg
ofReal_norm_eq_enorm' 📖	mathematical	—	ENNReal.ofReal Norm.norm SeminormedGroup.toNorm ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm	—	ENNReal.ofReal_eq_coe_nnreal norm_nonneg'
pow_mem_ball 📖	mathematical	Set Set.instMembership Metric.ball SeminormedCommGroup.toPseudoMetricSpace	Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup Real AddMonoid.toNatSMul Real.instAddMonoid	—	dist_eq_norm_div lt_of_le_of_lt norm_pow_le_mul_norm Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing nsmul_eq_mul lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.without_one_mul CancelDenoms.sub_subst CancelDenoms.mul_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le
pow_mem_closedBall 📖	mathematical	Set Set.instMembership Metric.closedBall SeminormedCommGroup.toPseudoMetricSpace	Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup Real AddMonoid.toNatSMul Real.instAddMonoid	—	dist_eq_norm_div LE.le.trans norm_pow_le_mul_norm nsmul_eq_mul mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing Nat.cast_nonneg
preimage_add_ball 📖	mathematical	—	Set.preimage AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace SubNegMonoid.toSub	—	Set.ext Set.mem_preimage Metric.mem_ball dist_eq_norm_sub sub_sub_eq_add_sub add_comm
preimage_add_closedBall 📖	mathematical	—	Set.preimage AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace SubNegMonoid.toSub	—	Set.ext Set.mem_preimage Metric.mem_closedBall dist_eq_norm_sub sub_sub_eq_add_sub add_comm
preimage_add_sphere 📖	mathematical	—	Set.preimage AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace SubNegMonoid.toSub	—	Set.ext Set.mem_preimage mem_sphere_iff_norm sub_sub_eq_add_sub add_comm
preimage_mul_ball 📖	mathematical	—	Set.preimage MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup Metric.ball SeminormedCommGroup.toPseudoMetricSpace DivInvMonoid.toDiv	—	Set.ext dist_eq_norm_div div_div_eq_mul_div mul_comm
preimage_mul_closedBall 📖	mathematical	—	Set.preimage MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup Metric.closedBall SeminormedCommGroup.toPseudoMetricSpace DivInvMonoid.toDiv	—	Set.ext dist_eq_norm_div div_div_eq_mul_div mul_comm
preimage_mul_sphere 📖	mathematical	—	Set.preimage MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup Metric.sphere SeminormedCommGroup.toPseudoMetricSpace DivInvMonoid.toDiv	—	Set.ext div_div_eq_mul_div mul_comm
smul_ball'' 📖	mathematical	—	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup MulAction.toSemigroupAction Monoid.toMulAction Metric.ball SeminormedCommGroup.toPseudoMetricSpace	—	Set.ext dist_eq_norm_div div_eq_inv_mul mul_inv_rev mul_assoc
smul_closedBall'' 📖	mathematical	—	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup MulAction.toSemigroupAction Monoid.toMulAction Metric.closedBall SeminormedCommGroup.toPseudoMetricSpace	—	Set.ext dist_eq_norm_div div_eq_inv_mul mul_inv_rev mul_assoc
toReal_coe_nnnorm 📖	mathematical	—	ENNReal.toReal ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Norm.norm SeminormedAddGroup.toNorm	—	—
toReal_coe_nnnorm' 📖	mathematical	—	ENNReal.toReal ENNReal.ofNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm Norm.norm SeminormedGroup.toNorm	—	—
toReal_enorm 📖	mathematical	—	ENNReal.toReal ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm Norm.norm SeminormedAddGroup.toNorm	—	—
toReal_enorm' 📖	mathematical	—	ENNReal.toReal ENorm.enorm NNNorm.toENorm SeminormedGroup.toNNNorm Norm.norm SeminormedGroup.toNorm	—	—
vadd_ball'' 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup AddAction.toAddSemigroupAction AddMonoid.toAddAction Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace	—	Set.ext Set.mem_vadd_set Metric.mem_ball dist_eq_norm_sub sub_eq_neg_add eq_neg_add_iff_add_eq neg_add_rev add_assoc
vadd_closedBall'' 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup AddAction.toAddSemigroupAction AddMonoid.toAddAction Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace	—	Set.ext Set.mem_vadd_set Metric.mem_closedBall dist_eq_norm_sub sub_eq_neg_add eq_neg_add_iff_add_eq neg_add_rev add_assoc
zero_lt_one_add_norm_sq 📖	mathematical	—	Real Real.instLT Real.instZero Real.instAdd Real.instOne Monoid.toNatPow Real.instMonoid Norm.norm SeminormedAddGroup.toNorm	—	add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul
zero_lt_one_add_norm_sq' 📖	mathematical	—	Real Real.instLT Real.instZero Real.instAdd Real.instOne Monoid.toNatPow Real.instMonoid Norm.norm SeminormedGroup.toNorm	—	add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul

---

← Back to Index