Normed

📁 Source: Mathlib/Topology/ContinuousMap/Bounded/Normed.lean

Statistics

Metric	Count
Definitions `compLeftContinuousBounded`, `C`, `hasNatPow`, `instAddCommGroup`, `instAlgebra`, `instCommRing`, `instInf`, `instIntCast_1`, `instLattice`, `instModule'`, `instNatCast_1`, `instNeg`, `instNonUnitalNormedCommRing`, `instNonUnitalNormedRing`, `instNonUnitalRing`, `instNonUnitalSeminormedCommRing`, `instNonUnitalSeminormedRing`, `instNorm`, `instNormedAddCommGroup`, `instNormedAlgebra`, `instNormedCommRing`, `instNormedRing`, `instNormedSpace`, `instPartialOrder`, `instRing`, `instSMul'`, `instSMulInt`, `instSemilatticeInf`, `instSemilatticeSup`, `instSeminormedAddCommGroup`, `instSeminormedCommRing`, `instSeminormedRing`, `instSup`, `nnnorm`, `nnrealPart`, `normComp`, `ofNormedAddCommGroup`, `ofNormedAddCommGroupDiscrete`, `toContinuousMapₐ`, `compLeftContinuousBounded`, `compLeftContinuousBounded`	41
Theorems `compLeftContinuousBounded_apply_apply`, `abs_diff_coe_le_dist`, `abs_self_eq_nnrealPart_add_nnrealPart_neg`, `add_norm_nonneg`, `algebraMap_apply`, `apply_le_norm`, `bddAbove_range_norm_comp`, `coe_abs`, `coe_inf`, `coe_intCast`, `coe_le_coe_add_dist`, `coe_natCast`, `coe_neg`, `coe_negPart`, `coe_normComp`, `coe_npowRec`, `coe_ofNat`, `coe_ofNormedAddCommGroup`, `coe_ofNormedAddCommGroupDiscrete`, `coe_posPart`, `coe_sup`, `coe_toContinuousMapₐ`, `coe_zsmul`, `coe_zsmulRec`, `dist_le_two_norm`, `dist_le_two_norm'`, `enorm_eq_iSup_enorm`, `instHasSolidNorm`, `instIsBoundedSMul_1`, `instIsOrderedAddMonoid`, `instIsScalarTower_1`, `instNormOneClass`, `instSMulCommClass_1`, `instSMulCommClass_2`, `mkOfCompact_neg`, `mkOfCompact_sub`, `neg_apply`, `neg_norm_le_apply`, `nndist_le_two_nnnorm`, `nnnorm_coeFn_eq`, `nnnorm_coe_le_nnnorm`, `nnnorm_const_eq`, `nnnorm_const_le`, `nnnorm_def`, `nnnorm_eq_iSup_nnnorm`, `nnnorm_le`, `nnrealPart_coeFn_eq`, `norm_coe_le_norm`, `norm_compContinuous_le`, `norm_const_eq`, `norm_const_le`, `norm_def`, `norm_eq`, `norm_eq_iSup_norm`, `norm_eq_of_nonempty`, `norm_eq_zero_of_empty`, `norm_le`, `norm_le_of_nonempty`, `norm_lt_iff_of_compact`, `norm_lt_iff_of_nonempty_compact`, `norm_normComp`, `norm_ofNormedAddCommGroup_le`, `norm_sub_nonneg`, `self_eq_nnrealPart_sub_nnrealPart_neg`, `toContinuousMapₐ_apply`, `zsmul_apply`, `compLeftContinuousBounded_apply`, `compLeftContinuousBounded_apply_apply`	68
Total	109

BoundedContinuousFunction

Definitions

Name	Category	Theorems
`C` 📖	CompOp	—
`hasNatPow` 📖	CompOp	1 math math: `tendsto_integral_mul_one_add_inv_smul_sq_pow`
`instAddCommGroup` 📖	CompOp	—
`instAlgebra` 📖	CompOp	13 math math: `algebraMap_apply`, `coe_toContinuousMapStarₐ`, `mem_charPoly`, `charAlgHom_apply`, `AlgHom.compLeftContinuousBounded_apply_apply`, `toContinuousMapStarₐ_apply_apply`, `coe_toContinuousMapₐ`, `toContinuousMapₐ_apply`, `coe_algEquiv_lpBCF_symm`, `separatesPoints_charPoly`, `coe_algEquiv_lpBCF`, `RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict`, `char_mem_charPoly`
`instCommRing` 📖	CompOp	—
`instInf` 📖	CompOp	1 math math: `coe_inf`
`instIntCast_1` 📖	CompOp	1 math math: `coe_intCast`
`instLattice` 📖	CompOp	4 math math: `coe_posPart`, `coe_abs`, `instHasSolidNorm`, `coe_negPart`
`instModule'` 📖	CompOp	—
`instNatCast_1` 📖	CompOp	1 math math: `coe_natCast`
`instNeg` 📖	CompOp	8 math math: `integral_eq_integral_nnrealPart_sub`, `coe_neg`, `abs_self_eq_nnrealPart_add_nnrealPart_neg`, `tendsto_integral_mul_one_add_inv_smul_sq_pow`, `neg_apply`, `mkOfCompact_neg`, `coe_zsmulRec`, `self_eq_nnrealPart_sub_nnrealPart_neg`
`instNonUnitalNormedCommRing` 📖	CompOp	—
`instNonUnitalNormedRing` 📖	CompOp	1 math math: `instCStarRing`
`instNonUnitalRing` 📖	CompOp	8 math math: `instSMulCommClass_1`, `compactlySupported_eq_top_of_isCompact`, `instSMulCommClass_2`, `compactlySupported_eq_top`, `instIsScalarTower_1`, `compactlySupported_eq_top_iff`, `mem_compactlySupported`, `ofCompactSupport_mem`
`instNonUnitalSeminormedCommRing` 📖	CompOp	—
`instNonUnitalSeminormedRing` 📖	CompOp	—
`instNorm` 📖	CompOp	41 math math: `tietze_extension_step`, `norm_compContinuous_le`, `exist_norm_eq`, `exists_extension_norm_eq_of_isClosedEmbedding`, `norm_toContinuousMap_eq`, `norm_eq`, `Real.abs_mulExpNegMulSq_comp_le_norm`, `norm_le`, `exists_norm_eq_restrict_eq_of_closed`, `neg_norm_le_apply`, `norm_le_of_nonempty`, `norm_integral_le_norm`, `apply_le_norm`, `norm_eq_zero_of_empty`, `Lp_norm_le`, `norm_lt_iff_of_compactlySupported`, `MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le`, `ZeroAtInftyContinuousMap.norm_toBCF_eq_norm`, `norm_def`, `norm_lt_iff_of_compact`, `norm_lt_iff_of_nonempty_compact`, `ContDiffMapSupportedIn.seminorm_apply`, `norm_coe_le_norm`, `norm_mkOfCompact`, `add_norm_nonneg`, `MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt`, `norm_sub_nonneg`, `norm_const_eq`, `norm_eq_of_nonempty`, `norm_integral_le_mul_norm`, `norm_normComp`, `MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral`, `norm_const_le`, `exists_norm_eq_restrict_eq`, `norm_lt_iff_of_nonempty_compactlySupported`, `norm_eq_iSup_norm`, `dist_le_two_norm`, `norm_ofNormedAddCommGroup_le`, `instNormOneClass`, `ContDiffMapSupportedIn.norm_toBoundedContinuousFunction`, `exists_extension_norm_eq_of_isClosedEmbedding'`
`instNormedAddCommGroup` 📖	CompOp	4 math math: `coe_posPart`, `coe_abs`, `instHasSolidNorm`, `coe_negPart`
`instNormedAlgebra` 📖	CompOp	—
`instNormedCommRing` 📖	CompOp	—
`instNormedRing` 📖	CompOp	—
`instNormedSpace` 📖	CompOp	2 math math: `ContinuousMap.toLp_norm_eq_toLp_norm_coe`, `toLp_norm_le`
`instPartialOrder` 📖	CompOp	3 math math: `instIsOrderedAddMonoid`, `add_norm_nonneg`, `norm_sub_nonneg`
`instRing` 📖	CompOp	—
`instSMul'` 📖	CompOp	1 math math: `instIsBoundedSMul_1`
`instSMulInt` 📖	CompOp	2 math math: `coe_zsmul`, `zsmul_apply`
`instSemilatticeInf` 📖	CompOp	—
`instSemilatticeSup` 📖	CompOp	—
`instSeminormedAddCommGroup` 📖	CompOp	22 math math: `lintegral_nnnorm_le`, `nnnorm_def`, `Lp_nnnorm_le`, `range_toLpHom`, `ContinuousMap.linearIsometryBoundedOfCompact_symm_apply`, `coe_lpBCFₗᵢ`, `ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv`, `ContinuousMap.toLp_def`, `nnnorm_const_eq`, `ContinuousMap.toLp_norm_eq_toLp_norm_coe`, `instNormedStarGroup`, `nnnorm_eq_iSup_nnnorm`, `nnnorm_coe_le_nnnorm`, `nnnorm_le`, `nnnorm_const_le`, `coe_lpBCFₗᵢ_symm`, `ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv`, `ContinuousMap.linearIsometryBoundedOfCompact_apply_apply`, `toLp_norm_le`, `enorm_eq_iSup_enorm`, `ContinuousMap.linearIsometryBoundedOfCompact_toIsometryEquiv`, `nndist_le_two_nnnorm`
`instSeminormedCommRing` 📖	CompOp	—
`instSeminormedRing` 📖	CompOp	—
`instSup` 📖	CompOp	1 math math: `coe_sup`
`nnnorm` 📖	CompOp	1 math math: `nnnorm_coeFn_eq`
`nnrealPart` 📖	CompOp	4 math math: `integral_eq_integral_nnrealPart_sub`, `abs_self_eq_nnrealPart_add_nnrealPart_neg`, `nnrealPart_coeFn_eq`, `self_eq_nnrealPart_sub_nnrealPart_neg`
`normComp` 📖	CompOp	2 math math: `coe_normComp`, `norm_normComp`
`ofNormedAddCommGroup` 📖	CompOp	2 math math: `coe_ofNormedAddCommGroup`, `norm_ofNormedAddCommGroup_le`
`ofNormedAddCommGroupDiscrete` 📖	CompOp	1 math math: `coe_ofNormedAddCommGroupDiscrete`
`toContinuousMapₐ` 📖	CompOp	3 math math: `coe_toContinuousMapₐ`, `toContinuousMapₐ_apply`, `RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_diff_coe_le_dist` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike` `Dist.dist` `instDist`	—	`dist_eq_norm` `norm_coe_le_norm` `instBoundedSub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`abs_self_eq_nnrealPart_add_nnrealPart_neg` 📖	mathematical	—	`Real` `abs` `Real.lattice` `Real.instAddGroup` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `instFunLike` `Pi.instAdd` `Real.instAdd` `NNReal` `NNReal.toReal` `instPseudoMetricSpaceNNReal` `nnrealPart` `instNeg` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	—	`max_zero_add_max_neg_zero_eq_abs_self` `Real.instIsOrderedAddMonoid`
`add_norm_nonneg` 📖	mathematical	—	`BoundedContinuousFunction` `Real` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Real.normedAddCommGroup` `Real.lattice` `instZero` `Real.instZero` `instAdd` `Real.instAdd` `instBoundedAddOfLipschitzAdd` `Real.instAddMonoid` `Real.hasLipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `const` `Norm.norm` `instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing`	—	`instBoundedAddOfLipschitzAdd` `Real.hasLipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.neg_congr` `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.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `abs_le` `Real.instIsOrderedAddMonoid` `norm_coe_le_norm`
`algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `instSemiring` `Ring.toSemiring` `NormedRing.toRing` `instBoundedMul` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `IsTopologicalSemiring.toContinuousMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.toSMul` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `Algebra.algebraMap_eq_smul_one`
`apply_le_norm` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `instFunLike` `Norm.norm` `instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	—	`abs_le` `Real.instIsOrderedAddMonoid` `norm_coe_le_norm`
`bddAbove_range_norm_comp` 📖	mathematical	—	`BddAbove` `Real` `Real.instLE` `Set.range` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike`	—	`Bornology.IsBounded.bddAbove` `Real.instIsOrderBornology` `isBounded_range`
`coe_abs` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instFunLike` `abs` `instLattice` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `instNormedAddCommGroup` `Pi.instLattice` `Pi.addGroup`	—	—
`coe_inf` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instFunLike` `instInf` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	—
`coe_intCast` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `instFunLike` `instIntCast_1` `Pi.instIntCast` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `SeminormedRing.toRing`	—	—
`coe_le_coe_add_dist` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `instFunLike` `Real.instAdd` `Dist.dist` `instDist`	—	`sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `abs_le` `dist_coe_le_dist`
`coe_natCast` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `instFunLike` `instNatCast_1` `Pi.instNatCast` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SeminormedRing.toRing`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`coe_negPart` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instFunLike` `NegPart.negPart` `instNegPart` `instLattice` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `instNormedAddCommGroup` `Pi.instLattice` `Pi.addGroup`	—	—
`coe_normComp` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `Real` `Real.pseudoMetricSpace` `instFunLike` `normComp` `Norm.norm` `SeminormedAddCommGroup.toNorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—
`coe_npowRec` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `instFunLike` `instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SeminormedRing.toRing` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instBoundedMul` `SeminormedRing.toNonUnitalSeminormedRing` `IsTopologicalSemiring.toContinuousMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `npowRec.eq_1` `pow_zero` `coe_one` `npowRec.eq_2` `pow_succ` `coe_mul`
`coe_ofNat` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `instFunLike`	—	—
`coe_ofNormedAddCommGroup` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `ofNormedAddCommGroup`	—	—
`coe_ofNormedAddCommGroupDiscrete` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike` `ofNormedAddCommGroupDiscrete`	—	—
`coe_posPart` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instFunLike` `PosPart.posPart` `instPosPart` `instLattice` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `instNormedAddCommGroup` `Pi.instLattice` `Pi.addGroup`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instFunLike` `instSup` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	—
`coe_toContinuousMapₐ` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ContinuousMap.instFunLike` `AlgHom` `BoundedContinuousFunction` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `instSemiring` `Ring.toSemiring` `NormedRing.toRing` `instBoundedMul` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `instAlgebra` `ContinuousMap.algebra` `NormedAlgebra.toAlgebra` `AlgHom.funLike` `toContinuousMapₐ` `instFunLike`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd`
`coe_zsmul` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike` `instSMulInt` `SubNegMonoid.toZSMul` `Pi.subNegMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	—
`coe_zsmulRec` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike` `zsmulRec` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `instBoundedAddOfLipschitzAdd` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instNeg` `instSMulNat` `SubNegMonoid.toZSMul` `Pi.subNegMonoid`	—	`instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `zsmulRec.eq_1` `coe_nsmul` `natCast_zsmul` `zsmulRec.eq_2` `negSucc_zsmul` `coe_neg`
`dist_le_two_norm` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Norm.norm` `instNorm`	—	`dist_le_two_norm'` `norm_coe_le_norm`
`dist_le_two_norm'` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_le_norm_add_norm` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `two_mul`
`enorm_eq_iSup_enorm` 📖	mathematical	—	`ENorm.enorm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `instSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `instFunLike`	—	`edist_eq_iSup`
`instHasSolidNorm` 📖	mathematical	—	`HasSolidNorm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNormedAddCommGroup` `instLattice`	—	`HasSolidNorm.solid` `norm_le` `norm_nonneg` `LE.le.trans` `norm_coe_le_norm`
`instIsBoundedSMul_1` 📖	mathematical	—	`IsBoundedSMul` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `instPseudoMetricSpace` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `instSMul'`	—	`IsBoundedSMul.of_norm_smul_le` `norm_ofNormedAddCommGroup_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg`
`instIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instPartialOrder`	—	`instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`
`instIsScalarTower_1` 📖	mathematical	—	`IsScalarTower` `BoundedContinuousFunction` `NonUnitalSeminormedRing.toPseudoMetricSpace` `instSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalSeminormedRing.toNonUnitalRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `instNonUnitalRing`	—	`instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `ext` `smul_mul_assoc`
`instNormOneClass` 📖	mathematical	—	`NormOneClass` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `instOne`	—	`norm_eq_iSup_norm` `NormOneClass.norm_one` `ciSup_const`
`instSMulCommClass_1` 📖	mathematical	—	`SMulCommClass` `BoundedContinuousFunction` `NonUnitalSeminormedRing.toPseudoMetricSpace` `instSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalSeminormedRing.toNonUnitalRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `instNonUnitalRing`	—	`instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `ext` `mul_smul_comm`
`instSMulCommClass_2` 📖	mathematical	—	`SMulCommClass` `BoundedContinuousFunction` `NonUnitalSeminormedRing.toPseudoMetricSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalSeminormedRing.toNonUnitalRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `instNonUnitalRing` `instSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `ext` `mul_smul_comm`
`mkOfCompact_neg` 📖	mathematical	—	`mkOfCompact` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ContinuousMap.instNegOfContinuousNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoundedContinuousFunction` `instNeg`	—	`IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`mkOfCompact_sub` 📖	mathematical	—	`mkOfCompact` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ContinuousMap.instSubOfContinuousSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoundedContinuousFunction` `instSub` `instBoundedSub`	—	`IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`neg_norm_le_apply` 📖	mathematical	—	`Real` `Real.instLE` `Real.instNeg` `Norm.norm` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `DFunLike.coe` `instFunLike`	—	`abs_le` `Real.instIsOrderedAddMonoid` `norm_coe_le_norm`
`nndist_le_two_nnnorm` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instSeminormedAddCommGroup`	—	`dist_le_two_norm`
`nnnorm_coeFn_eq` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `instFunLike` `nnnorm` `Real` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.pseudoMetricSpace`	—	—
`nnnorm_coe_le_nnnorm` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike` `instSeminormedAddCommGroup`	—	`norm_coe_le_norm`
`nnnorm_const_eq` 📖	mathematical	—	`NNNorm.nnnorm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instSeminormedAddCommGroup` `const`	—	`norm_const_eq`
`nnnorm_const_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instSeminormedAddCommGroup` `const`	—	`norm_const_le`
`nnnorm_def` 📖	mathematical	—	`NNNorm.nnnorm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instSeminormedAddCommGroup` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `instPseudoMetricSpace` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`nnnorm_eq_iSup_nnnorm` 📖	mathematical	—	`NNNorm.nnnorm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instSeminormedAddCommGroup` `iSup` `NNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `NNReal.instConditionallyCompleteLinearOrderBot` `DFunLike.coe` `instFunLike`	—	`norm_eq_iSup_norm` `NNReal.coe_iSup`
`nnnorm_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instSeminormedAddCommGroup` `DFunLike.coe` `instFunLike`	—	`norm_le` `Subtype.prop`
`nnrealPart_coeFn_eq` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `instFunLike` `nnrealPart` `Real` `Real.toNNReal` `Real.pseudoMetricSpace`	—	—
`norm_coe_le_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike` `instNorm`	—	`dist_zero_right` `dist_coe_le_dist`
`norm_compContinuous_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `compContinuous`	—	`LE.le.trans` `LipschitzWith.dist_le_mul` `lipschitz_compContinuous` `NNReal.coe_one` `one_mul` `dist_zero_right` `le_refl`
`norm_const_eq` 📖	mathematical	—	`Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `const` `SeminormedAddCommGroup.toNorm`	—	`le_antisymm` `norm_const_le` `norm_coe_le_norm`
`norm_const_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `const` `SeminormedAddCommGroup.toNorm`	—	`norm_le` `norm_nonneg` `le_rfl`
`norm_def` 📖	mathematical	—	`Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `Dist.dist` `instDist` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`norm_eq` 📖	mathematical	—	`Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `InfSet.sInf` `Real` `Real.instInfSet` `setOf` `Real.instLE` `Real.instZero`	—	`dist_zero_right`
`norm_eq_iSup_norm` 📖	mathematical	—	`Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `iSup` `Real` `Real.instSupSet` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `instFunLike`	—	`dist_eq_iSup` `dist_zero_right`
`norm_eq_of_nonempty` 📖	mathematical	—	`Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `InfSet.sInf` `Real` `Real.instInfSet` `setOf`	—	`norm_eq` `le_trans` `norm_nonneg`
`norm_eq_zero_of_empty` 📖	mathematical	—	`Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `Real` `Real.instZero`	—	`dist_zero_of_empty`
`norm_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `instFunLike`	—	`dist_zero_right` `dist_le`
`norm_le_of_nonempty` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `instFunLike`	—	`dist_le_iff_of_nonempty`
`norm_lt_iff_of_compact` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `instFunLike`	—	`dist_lt_iff_of_compact`
`norm_lt_iff_of_nonempty_compact` 📖	mathematical	—	`Real` `Real.instLT` `Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instNorm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `instFunLike`	—	`dist_lt_iff_of_nonempty_compact`
`norm_normComp` 📖	mathematical	—	`Norm.norm` `BoundedContinuousFunction` `Real` `Real.pseudoMetricSpace` `instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `normComp` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`norm_eq` `norm_norm`
`norm_ofNormedAddCommGroup_le` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instLE` `Real.instZero` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`BoundedContinuousFunction` `instNorm` `ofNormedAddCommGroup`	—	`norm_le`
`norm_sub_nonneg` 📖	mathematical	—	`BoundedContinuousFunction` `Real` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Real.normedAddCommGroup` `Real.lattice` `instZero` `Real.instZero` `instSub` `Real.instSub` `instBoundedSub` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `IsTopologicalAddGroup.to_continuousSub` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.instAddGroup` `instIsTopologicalAddGroupReal` `const` `Norm.norm` `instNorm`	—	`instBoundedSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `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.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `abs_le` `norm_coe_le_norm`
`self_eq_nnrealPart_sub_nnrealPart_neg` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `Real` `Real.pseudoMetricSpace` `instFunLike` `Pi.instSub` `Real.instSub` `NNReal` `NNReal.toReal` `instPseudoMetricSpaceNNReal` `nnrealPart` `instNeg` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	—	`max_zero_sub_max_neg_zero_eq_self` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`toContinuousMapₐ_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `instSemiring` `Ring.toSemiring` `NormedRing.toRing` `instBoundedMul` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `instAlgebra` `ContinuousMap.algebra` `NormedAlgebra.toAlgebra` `AlgHom.funLike` `toContinuousMapₐ` `toContinuousMap` `instFunLike`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd`
`zsmul_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike` `instSMulInt` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	—

BoundedContinuousFunction.AlgHom

Definitions

Name	Category	Theorems
`compLeftContinuousBounded` 📖	CompOp	2 math math: `compLeftContinuousBounded_apply_apply`, `RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLeftContinuousBounded_apply_apply` 📖	mathematical	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedRing.toMetricSpace` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Ring.toSemiring` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing` `AlgHom.funLike`	`BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `BoundedContinuousFunction.instFunLike` `BoundedContinuousFunction.instSemiring` `instBoundedMul` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `IsTopologicalSemiring.toContinuousMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `BoundedContinuousFunction.instAlgebra` `compLeftContinuousBounded`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd`

ContinuousLinearMap

Definitions

Name	Category	Theorems
`compLeftContinuousBounded` 📖	CompOp	1 math math: `compLeftContinuousBounded_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLeftContinuousBounded_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `BoundedContinuousFunction.instFunLike` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `BoundedContinuousFunction.instPseudoMetricSpace` `BoundedContinuousFunction.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoundedContinuousFunction.instModule` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `NormedSpace.toIsBoundedSMul` `funLike` `compLeftContinuousBounded`	—	`instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NormedSpace.toIsBoundedSMul`

RingHom

Definitions

Name	Category	Theorems
`compLeftContinuousBounded` 📖	CompOp	1 math math: `compLeftContinuousBounded_apply_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLeftContinuousBounded_apply_apply` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedRing.toPseudoMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `instFunLike`	`BoundedContinuousFunction` `BoundedContinuousFunction.instFunLike` `BoundedContinuousFunction.instSemiring` `instBoundedMul` `SeminormedRing.toNonUnitalSeminormedRing` `IsTopologicalSemiring.toContinuousMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `compLeftContinuousBounded`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd`

---

← Back to Index