Basic

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

Statistics

Metric	Count
Definitions `compLeftContinuousBounded`, `apply`, `codRestrict`, `coeFnAddHom`, `coeFnAddMonoidHom`, `coeFnMonoidHom`, `comp`, `compContinuous`, `const`, `evalCLM`, `extend`, `indicator`, `instAdd`, `instAddCommMonoid`, `instAddMonoid`, `instAddZeroClass`, `instCoeTC`, `instCommMonoid`, `instDist`, `instDistribMulAction`, `instFunLike`, `instInhabited`, `instIntCast`, `instMetricSpace`, `instModule`, `instMonoid`, `instMul`, `instMulAction`, `instMulOneClass`, `instNatCast`, `instOne`, `instPow`, `instPseudoMetricSpace`, `instSMul`, `instSMulNat`, `instSemiring`, `instSub`, `instZero`, `mkOfBound`, `mkOfCompact`, `mkOfDiscrete`, `restrict`, `toContinuousMap`, `toContinuousMapAddHom`, `toContinuousMapAddMonoidHom`, `toContinuousMapLinearMap`, `toContinuousMapMonoidHom`, `«term_→ᵇ_»`, `BoundedContinuousMapClass`, `compLeftContinuousBounded`	50
Theorems `compLeftContinuousBounded_apply`, `upper_bound`, `add_apply`, `add_compContinuous`, `bounded`, `coeFnAddMonoidHom_apply`, `coeFnMonoidHom_apply`, `coe_add`, `coe_compContinuous`, `coe_mk`, `coe_mul`, `coe_nsmul`, `coe_nsmulRec`, `coe_one`, `coe_pow`, `coe_prod`, `coe_restrict`, `coe_smul`, `coe_sub`, `coe_sum`, `coe_toContinuousMap`, `coe_zero`, `compContinuous_apply`, `comp_apply`, `const_apply`, `const_apply'`, `continuous`, `continuous_coe`, `continuous_comp`, `continuous_compContinuous`, `continuous_eval`, `continuous_eval_const`, `dist_coe_le_dist`, `dist_eq`, `dist_eq_iSup`, `dist_extend_extend`, `dist_le`, `dist_le_iff_of_nonempty`, `dist_lt_iff_of_compact`, `dist_lt_iff_of_nonempty_compact`, `dist_lt_of_nonempty_compact`, `dist_set_exists`, `dist_zero_of_empty`, `edist_eq_iSup`, `eq_of_empty`, `evalCLM_apply`, `ext`, `ext_iff`, `extend_apply`, `extend_apply'`, `extend_comp`, `extend_of_empty`, `forall_coe_one_iff_one`, `forall_coe_zero_iff_zero`, `indicator_apply`, `instBoundedContinuousMapClass`, `instCompleteSpace`, `instContinuousEval`, `instContinuousEvalConst`, `instIsBoundedSMul`, `instIsCentralScalar`, `instIsScalarTower`, `instLipschitzAdd`, `instSMulCommClass`, `intCast_apply`, `isBounded_image`, `isBounded_range`, `isEmbedding_coeFn`, `isInducing_coeFn`, `isometry_extend`, `lipschitz_comp`, `lipschitz_compContinuous`, `lipschitz_eval_const`, `lipschitz_evalx`, `map_bounded'`, `mkOfBound_coe`, `mkOfCompact_add`, `mkOfCompact_apply`, `mkOfCompact_one`, `mkOfCompact_zero`, `mkOfDiscrete_apply`, `mul_apply`, `natCast_apply`, `nndist_coe_le_nndist`, `nndist_eq`, `nndist_eq_iSup`, `nndist_set_exists`, `nsmul_apply`, `one_compContinuous`, `pow_apply`, `prod_apply`, `restrict_apply`, `smul_apply`, `sub_apply`, `sum_apply`, `tendsto_iff_tendstoUniformly`, `toContinuousMapAddMonoidHom_apply`, `toContinuousMapLinearMap_apply`, `toContinuousMapMonoidHom_apply`, `uniformContinuous_coe`, `uniformContinuous_comp`, `zero_compContinuous`, `map_bounded`, `toContinuousMapClass`, `compLeftContinuousBounded_apply`	105
Total	155

AddMonoidHom

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLeftContinuousBounded_apply` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike`	`BoundedContinuousFunction` `BoundedContinuousFunction.instAddZeroClass` `compLeftContinuousBounded` `BoundedContinuousFunction.comp`	—	—

BoundedContinuousFunction

Definitions

Name	Category	Theorems
`codRestrict` 📖	CompOp	—
`coeFnAddHom` 📖	CompOp	—
`coeFnAddMonoidHom` 📖	CompOp	1 math math: `coeFnAddMonoidHom_apply`
`coeFnMonoidHom` 📖	CompOp	1 math math: `coeFnMonoidHom_apply`
`comp` 📖	CompOp	6 math math: `uniformContinuous_comp`, `comp_apply`, `lipschitz_comp`, `AddMonoidHom.compLeftContinuousBounded_apply`, `MonoidHom.compLeftContinuousBounded_apply`, `continuous_comp`
`compContinuous` 📖	CompOp	10 math math: `tietze_extension_step`, `norm_compContinuous_le`, `continuous_compContinuous`, `zero_compContinuous`, `one_compContinuous`, `compContinuous_apply`, `lipschitz_compContinuous`, `coe_compContinuous`, `add_compContinuous`, `exists_extension_norm_eq_of_isClosedEmbedding'`
`const` 📖	CompOp	11 math math: `integral_const_sub`, `MeasureTheory.FiniteMeasure.testAgainstNN_const`, `nnnorm_const_eq`, `const_apply'`, `nnnorm_const_le`, `integral_add_const`, `add_norm_nonneg`, `norm_sub_nonneg`, `norm_const_eq`, `norm_const_le`, `const_apply`
`evalCLM` 📖	CompOp	1 math math: `evalCLM_apply`
`extend` 📖	CompOp	6 math math: `isometry_extend`, `dist_extend_extend`, `extend_apply'`, `extend_of_empty`, `extend_comp`, `extend_apply`
`indicator` 📖	CompOp	1 math math: `indicator_apply`
`instAdd` 📖	CompOp	17 math math: `ContinuousMap.addEquivBoundedOfCompact_apply`, `mkOfCompact_add`, `coe_nsmulRec`, `coe_ringEquiv_lpBCF`, `MeasureTheory.FiniteMeasure.testAgainstNN_add`, `tendsto_integral_mul_one_add_inv_smul_sq_pow`, `add_apply`, `coe_add`, `coe_addEquiv_lpBCF_symm`, `coe_zsmulRec`, `coe_addEquiv_lpBCF`, `ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv`, `integral_add_const`, `add_norm_nonneg`, `ContinuousMap.addEquivBoundedOfCompact_symm_apply`, `coe_ringEquiv_lpBCF_symm`, `add_compContinuous`
`instAddCommMonoid` 📖	CompOp	51 math math: `MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply`, `ContDiffMapSupportedIn.structureMapCLM_eq_of_scalars`, `ContDiffMapSupportedIn.structureMapCLM_apply`, `TestFunction.toBoundedContinuousFunctionCLM_eq_of_scalars`, `evalCLM_apply`, `toContinuousMapLinearMap_apply`, `TestFunction.toBoundedContinuousFunctionCLM_apply`, `MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN`, `instIsOrderedAddMonoid`, `MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto`, `SchwartzMap.toBoundedContinuousFunctionCLM_apply`, `ContDiffMapSupportedIn.structureMapLM_eq_of_scalars`, `toLp_inj`, `toLp_injective`, `ContDiffMapSupportedIn.uniformSpace_eq_iInf`, `ContDiffMapSupportedIn.continuous_iff_comp_withOrder`, `ContDiffMapSupportedIn.structureMapCLM_zero_apply`, `ContinuousMap.toLp_def`, `coe_sum`, `ContDiffMapSupportedIn.structureMapLM_apply_withOrder`, `ContinuousMap.toLp_norm_eq_toLp_norm_coe`, `coeFn_toLp`, `ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM`, `ContDiffMapSupportedIn.toBoundedContinuousFunctionLM_eq_of_scalars`, `MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply`, `MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN`, `ContDiffMapSupportedIn.structureMapCLM_apply_withOrder`, `ContDiffMapSupportedIn.seminorm_apply`, `ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_eq_of_scalars`, `ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv`, `ContinuousLinearMap.compLeftContinuousBounded_apply`, `ContinuousMap.toLp_comp_toContinuousMap`, `ContDiffMapSupportedIn.structureMapLM_zero_injective`, `toLp_norm_le`, `MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous`, `ContDiffMapSupportedIn.toBoundedContinuousFunctionLM_apply`, `MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous`, `MeasureTheory.BoundedContinuousFunction.inner_toLp`, `ContDiffMapSupportedIn.continuous_iff_comp`, `MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN`, `sum_apply`, `ContDiffMapSupportedIn.structureMapCLM_zero_injective`, `ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_apply`, `ContDiffMapSupportedIn.structureMapLM_zero_apply`, `MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN`, `range_toLp`, `TestFunction.injective_toBoundedContinuousFunctionCLM`, `ContDiffMapSupportedIn.structureMapLM_apply`, `toLp_denseRange`, `MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto`, `ContDiffMapSupportedIn.structureMapLM_eq`
`instAddMonoid` 📖	CompOp	12 math math: `mkOfCompact_star`, `char_neg`, `coe_toContinuousMapStarₐ`, `instStarModule`, `toContinuousMapAddMonoidHom_apply`, `coeFnAddMonoidHom_apply`, `toContinuousMapStarₐ_apply_apply`, `star_mem_range_charAlgHom`, `star_apply`, `coe_star`, `ContinuousMap.addEquivBoundedOfCompact_symm_apply`, `instLipschitzAdd`
`instAddZeroClass` 📖	CompOp	4 math math: `instSMulCommClass_1`, `instSMulCommClass_2`, `instIsScalarTower_1`, `AddMonoidHom.compLeftContinuousBounded_apply`
`instCoeTC` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	2 math math: `prod_apply`, `coe_prod`
`instDist` 📖	CompOp	17 math math: `tietze_extension_step`, `dist_eq_iSup`, `dist_le`, `dist_toContinuousMap`, `ZeroAtInftyContinuousMap.dist_toBCF_eq_dist`, `dist_eq`, `dist_lt_iff_of_nonempty_compact`, `dist_coe_le_dist`, `dist_zero_of_empty`, `dist_le_iff_of_nonempty`, `norm_def`, `dist_extend_extend`, `abs_diff_coe_le_dist`, `dist_lt_of_nonempty_compact`, `coe_le_coe_add_dist`, `dist_mkOfCompact`, `dist_lt_iff_of_compact`
`instDistribMulAction` 📖	CompOp	—
`instFunLike` 📖	CompOp	229 math math: `MeasureTheory.Measure.exists_innerRegular_eq_of_isCompact`, `ContDiffMapSupportedIn.coe_toBoundedContinuousFunction`, `MeasureTheory.tendsto_integral_thickenedIndicator_of_isClosed`, `RingHom.compLeftContinuousBounded_apply_apply`, `forall_coe_zero_iff_zero`, `dist_eq_iSup`, `coe_zsmul`, `thickenedIndicator_mono_infEDist`, `coe_one`, `algebraMap_apply`, `integral_eq_integral_nnrealPart_sub`, `MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply`, `thickenedIndicator_one_of_mem_closure`, `ContDiffMapSupportedIn.structureMapCLM_apply`, `dist_le`, `indicator_apply`, `exist_norm_eq`, `coe_neg`, `coe_normComp`, `evalCLM_apply`, `nsmul_apply`, `CompactlySupportedContinuousMap.toBoundedContinuousFunction_apply`, `coe_mul`, `MeasureTheory.ProbabilityMeasure.continuous_lintegral_boundedContinuousFunction`, `isEmbedding_coeFn`, `MeasureTheory.MemLp.exists_boundedContinuous_integral_rpow_sub_le`, `coe_toContinuousMapStarₐ`, `coe_nsmulRec`, `restrict_apply`, `thickenedIndicator_zero`, `integral_const_sub`, `HasOuterApproxClosed.tendsto_apprSeq`, `coe_smul`, `thickenedIndicator_le_one`, `MeasureTheory.integrable_thickenedIndicator`, `exists_extension_norm_eq_of_isClosedEmbedding`, `lintegral_nnnorm_le`, `mem_charPoly`, `charAlgHom_apply`, `coe_intCast`, `coe_posPart`, `lintegral_lt_top_of_nnreal`, `MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto`, `isBounded_range`, `SchwartzMap.toBoundedContinuousFunctionCLM_apply`, `bddAbove_range_norm_comp`, `sub_apply`, `nndist_set_exists`, `lipschitzWith_thickenedIndicator`, `coe_natCast`, `MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq`, `comp_apply`, `integrable`, `pow_apply`, `MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto`, `exists_bounded_zero_one_of_closed`, `ContDiffMapSupportedIn.structureMapCLM_zero_apply`, `memLp_top`, `Real.abs_mulExpNegMulSq_comp_le_norm`, `coe_ringEquiv_lpBCF`, `MeasureTheory.Integrable.exists_boundedContinuous_lintegral_sub_le`, `ZeroAtInftyContinuousMap.toBCF_apply`, `norm_le`, `coe_lpBCFₗᵢ`, `AlgHom.compLeftContinuousBounded_apply_apply`, `mkOfCompact_apply`, `innerProbChar_apply`, `MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_lintegral`, `neg_norm_le_apply`, `coe_sum`, `dist_lt_iff_of_nonempty_compact`, `MeasureTheory.Integrable.exists_boundedContinuous_integral_sub_le`, `HasOuterApproxClosed.measure_le_lintegral`, `indicator_le_thickenedIndicator`, `uniformContinuous_coe`, `abs_self_eq_nnrealPart_add_nnrealPart_neg`, `ContDiffMapSupportedIn.structureMapLM_apply_withOrder`, `nnrealPart_coeFn_eq`, `continuous`, `UniformFun.isometry_ofFun_boundedContinuousFunction`, `exists_extension_forall_exists_le_ge_of_isClosedEmbedding`, `coe_ofNormedAddCommGroupDiscrete`, `norm_le_of_nonempty`, `tendsto_integral_mul_one_add_inv_smul_sq_pow`, `norm_integral_le_norm`, `apply_le_norm`, `add_apply`, `coe_add`, `dist_coe_le_dist`, `instContinuousEvalConst`, `measure_le_lintegral_thickenedIndicator`, `coe_sup`, `one_le_thickenedIndicator_apply'`, `tendsto_integral_mulExpNegMulSq_comp`, `SchwartzMap.toBoundedContinuousFunction_apply`, `MeasureTheory.integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure`, `neg_apply`, `coeFnAddMonoidHom_apply`, `exists_bounded_mem_Icc_of_closed_of_le`, `continuous_coe`, `thickenedIndicator_tendsto_indicator_closure`, `const_apply'`, `norm_lt_iff_of_compactlySupported`, `mem_compactlySupported`, `coeFn_toLp`, `prod_apply`, `MeasureTheory.ProbabilityMeasure.continuous_integral_boundedContinuousFunction`, `MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto`, `nndist_coe_le_nndist`, `HasOuterApproxClosed.apprSeq_apply_eq_one`, `nndist_eq_iSup`, `coe_ofNat`, `instContinuousEval`, `MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_lintegral`, `MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply`, `coe_abs`, `HasOuterApproxClosed.tendsto_lintegral_apprSeq`, `lintegral_of_real_lt_top`, `dist_le_iff_of_nonempty`, `CompletelyRegularSpace.exists_BCNN`, `coe_mk`, `forall_coe_one_iff_one`, `coe_addEquiv_lpBCF_symm`, `norm_lt_iff_of_compact`, `thickenedIndicator_subset`, `nnnorm_eq_iSup_nnnorm`, `nnnorm_coe_le_nnnorm`, `thickenedIndicator_apply`, `coe_restrict`, `ContDiffMapSupportedIn.structureMapCLM_apply_withOrder`, `norm_lt_iff_of_nonempty_compact`, `nnnorm_le`, `GromovHausdorff.HD_below_aux2`, `coeFnMonoidHom_apply`, `coe_lpBCFₗᵢ_symm`, `coe_zsmulRec`, `MeasureTheory.tendsto_lintegral_thickenedIndicator_of_isClosed`, `coe_addEquiv_lpBCF`, `MeasureTheory.Measure.exists_regular_eq_of_compactSpace`, `edist_eq_iSup`, `thickenedIndicator_mono_infEdist`, `ContinuousLinearMap.compLeftContinuousBounded_apply`, `compContinuous_apply`, `toContinuousMapStarₐ_apply_apply`, `norm_coe_le_norm`, `isBounded_range_integral`, `integral_add_const`, `star_apply`, `nnnorm_coeFn_eq`, `ContinuousMap.linearIsometryBoundedOfCompact_apply_apply`, `dist_set_exists`, `natCast_apply`, `coe_star`, `toReal_lintegral_coe_eq_integral`, `extend_apply'`, `coe_ofNormedAddCommGroup`, `coe_toContinuousMapₐ`, `MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_integral`, `mul_apply`, `intCast_apply`, `MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le`, `coe_nsmul`, `bounded`, `MeasureTheory.FiniteMeasure.continuous_integral_boundedContinuousFunction`, `abs_diff_coe_le_dist`, `HasOuterApproxClosed.indicator_le_apprSeq`, `measurable_coe_ennreal_comp`, `norm_integral_le_mul_norm`, `toContinuousMapₐ_apply`, `coe_inf`, `MeasureTheory.BoundedContinuousFunction.inner_toLp`, `mkOfBound_coe`, `coe_negPart`, `thickenedIndicator_one`, `coe_ringEquiv_lpBCF_symm`, `lipschitz_eval_const`, `zsmul_apply`, `sum_apply`, `TestFunction.coe_toBoundedContinuousFunction`, `coe_le_coe_add_dist`, `coe_zero`, `lipschitz_evalx`, `charMonoidHom_apply`, `const_apply`, `MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_integral`, `MeasureTheory.charFun_eq_integral_innerProbChar`, `coe_algEquiv_lpBCF_symm`, `coe_sub`, `extend_comp`, `norm_lt_iff_of_nonempty_compactlySupported`, `norm_eq_iSup_norm`, `enorm_eq_iSup_enorm`, `ContDiffMapSupportedIn.structureMapLM_zero_apply`, `smul_apply`, `mkOfDiscrete_apply`, `dist_le_two_norm`, `coe_npowRec`, `one_le_thickenedIndicator_apply`, `coe_prod`, `HasOuterApproxClosed.apprSeq_apply_le_one`, `coe_pow`, `tendsto_iff_tendstoUniformly`, `MeasureTheory.tendsto_integral_meas_thickening_le`, `self_eq_nnrealPart_sub_nnrealPart_neg`, `dist_lt_iff_of_compact`, `HasOuterApproxClosed.exAppr`, `coe_algEquiv_lpBCF`, `ContDiffMapSupportedIn.structureMapLM_apply`, `ext_iff`, `isBounded_image`, `apply_le_nndist_zero`, `MeasureTheory.FiniteMeasure.continuous_lintegral_boundedContinuousFunction`, `nndist_le_two_nnnorm`, `NNReal.upper_bound`, `coe_toContinuousMap`, `instBoundedContinuousMapClass`, `MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_rclike_tendsto`, `lintegral_le_edist_mul`, `coe_compContinuous`, `MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto`, `thickenedIndicator.coeFn_eq_comp`, `probCharDual_apply`, `GromovHausdorff.HD_below_aux1`, `char_apply`, `isInducing_coeFn`, `MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto`, `extend_apply`, `thickenedIndicator_mono`, `integrable_of_nnreal`
`instInhabited` 📖	CompOp	—
`instIntCast` 📖	CompOp	1 math math: `intCast_apply`
`instMetricSpace` 📖	CompOp	3 math math: `MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz`, `MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz`, `lintegral_le_edist_mul`
`instModule` 📖	CompOp	54 math math: `MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply`, `ContDiffMapSupportedIn.structureMapCLM_eq_of_scalars`, `ContDiffMapSupportedIn.structureMapCLM_apply`, `TestFunction.toBoundedContinuousFunctionCLM_eq_of_scalars`, `evalCLM_apply`, `toContinuousMapLinearMap_apply`, `TestFunction.toBoundedContinuousFunctionCLM_apply`, `MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN`, `MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto`, `SchwartzMap.toBoundedContinuousFunctionCLM_apply`, `ContDiffMapSupportedIn.structureMapLM_eq_of_scalars`, `toLp_inj`, `toLp_injective`, `ContDiffMapSupportedIn.uniformSpace_eq_iInf`, `ContDiffMapSupportedIn.continuous_iff_comp_withOrder`, `ContDiffMapSupportedIn.structureMapCLM_zero_apply`, `ContinuousMap.linearIsometryBoundedOfCompact_symm_apply`, `coe_lpBCFₗᵢ`, `ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv`, `ContinuousMap.toLp_def`, `ContDiffMapSupportedIn.structureMapLM_apply_withOrder`, `ContinuousMap.toLp_norm_eq_toLp_norm_coe`, `coeFn_toLp`, `ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM`, `ContDiffMapSupportedIn.toBoundedContinuousFunctionLM_eq_of_scalars`, `MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply`, `MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN`, `ContDiffMapSupportedIn.structureMapCLM_apply_withOrder`, `ContDiffMapSupportedIn.seminorm_apply`, `coe_lpBCFₗᵢ_symm`, `ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_eq_of_scalars`, `ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv`, `ContinuousLinearMap.compLeftContinuousBounded_apply`, `ContinuousMap.toLp_comp_toContinuousMap`, `ContinuousMap.linearIsometryBoundedOfCompact_apply_apply`, `ContDiffMapSupportedIn.structureMapLM_zero_injective`, `toLp_norm_le`, `MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous`, `ContDiffMapSupportedIn.toBoundedContinuousFunctionLM_apply`, `MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous`, `MeasureTheory.BoundedContinuousFunction.inner_toLp`, `ContDiffMapSupportedIn.continuous_iff_comp`, `MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN`, `ContDiffMapSupportedIn.structureMapCLM_zero_injective`, `ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_apply`, `ContDiffMapSupportedIn.structureMapLM_zero_apply`, `MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN`, `range_toLp`, `ContinuousMap.linearIsometryBoundedOfCompact_toIsometryEquiv`, `TestFunction.injective_toBoundedContinuousFunctionCLM`, `ContDiffMapSupportedIn.structureMapLM_apply`, `toLp_denseRange`, `MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto`, `ContDiffMapSupportedIn.structureMapLM_eq`
`instMonoid` 📖	CompOp	2 math math: `toContinuousMapMonoidHom_apply`, `coeFnMonoidHom_apply`
`instMul` 📖	CompOp	7 math math: `coe_mul`, `coe_ringEquiv_lpBCF`, `tendsto_integral_mul_one_add_inv_smul_sq_pow`, `mul_apply`, `coe_ringEquiv_lpBCF_symm`, `coe_npowRec`, `char_add_eq_mul`
`instMulAction` 📖	CompOp	—
`instMulOneClass` 📖	CompOp	2 math math: `MonoidHom.compLeftContinuousBounded_apply`, `charMonoidHom_apply`
`instNatCast` 📖	CompOp	1 math math: `natCast_apply`
`instOne` 📖	CompOp	11 math math: `coe_one`, `char_zero_eq_one`, `innerProbChar_zero`, `probCharDual_zero`, `tendsto_integral_mul_one_add_inv_smul_sq_pow`, `one_compContinuous`, `forall_coe_one_iff_one`, `MeasureTheory.FiniteMeasure.testAgainstNN_one`, `mkOfCompact_one`, `coe_npowRec`, `instNormOneClass`
`instPow` 📖	CompOp	2 math math: `pow_apply`, `coe_pow`
`instPseudoMetricSpace` 📖	CompOp	78 math math: `ContinuousMap.isUniformInducing_equivBoundedOfCompact`, `arzela_ascoli₁`, `MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply`, `ContDiffMapSupportedIn.structureMapCLM_eq_of_scalars`, `ContDiffMapSupportedIn.structureMapCLM_apply`, `TestFunction.toBoundedContinuousFunctionCLM_eq_of_scalars`, `evalCLM_apply`, `continuous_compContinuous`, `TestFunction.toBoundedContinuousFunctionCLM_apply`, `isEmbedding_coeFn`, `uniformContinuous_comp`, `MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN`, `ZeroAtInftyContinuousMap.isClosed_range_toBCF`, `MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto`, `SchwartzMap.toBoundedContinuousFunctionCLM_apply`, `nnnorm_def`, `toLp_inj`, `toLp_injective`, `ContDiffMapSupportedIn.uniformSpace_eq_iInf`, `arzela_ascoli`, `ContDiffMapSupportedIn.continuous_iff_comp_withOrder`, `ContDiffMapSupportedIn.structureMapCLM_zero_apply`, `lipschitz_comp`, `ContinuousMap.toLp_def`, `uniformContinuous_coe`, `isometry_extend`, `UniformFun.isometry_ofFun_boundedContinuousFunction`, `instContinuousEvalConst`, `ContinuousMap.toLp_norm_eq_toLp_norm_coe`, `continuous_coe`, `coeFn_toLp`, `nndist_coe_le_nndist`, `nndist_eq_iSup`, `ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM`, `instContinuousEval`, `MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply`, `MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN`, `instIsBoundedSMul_1`, `ContDiffMapSupportedIn.structureMapCLM_apply_withOrder`, `ContDiffMapSupportedIn.seminorm_apply`, `TopologicalSpace.exists_isInducing_l_infty`, `edist_eq_iSup`, `ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_eq_of_scalars`, `ContinuousLinearMap.compLeftContinuousBounded_apply`, `ContinuousMap.toLp_comp_toContinuousMap`, `ZeroAtInftyContinuousMap.isometry_toBCF`, `instIsBoundedSMul`, `lipschitz_compContinuous`, `ContinuousMap.isometryEquivBoundedOfCompact_toEquiv`, `toLp_norm_le`, `MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous`, `nndist_eq`, `MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous`, `MeasureTheory.BoundedContinuousFunction.inner_toLp`, `TopologicalSpace.exists_embedding_l_infty`, `lipschitz_eval_const`, `ContDiffMapSupportedIn.continuous_iff_comp`, `MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN`, `ContDiffMapSupportedIn.structureMapCLM_zero_injective`, `ContinuousMap.isometryEquivBoundedOfCompact_symm_apply`, `instLipschitzAdd`, `lipschitz_evalx`, `ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_apply`, `MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz_estimate`, `instCompleteSpace`, `ContinuousMap.isometryEquivBoundedOfCompact_apply`, `MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN`, `range_toLp`, `TestFunction.injective_toBoundedContinuousFunctionCLM`, `tendsto_iff_tendstoUniformly`, `ContinuousMap.isUniformEmbedding_equivBoundedOfCompact`, `apply_le_nndist_zero`, `toLp_denseRange`, `NNReal.upper_bound`, `MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto`, `continuous_comp`, `isInducing_coeFn`, `arzela_ascoli₂`
`instSMul` 📖	CompOp	12 math math: `instSMulCommClass_1`, `instSMulCommClass_2`, `instIsCentralScalar`, `coe_smul`, `instStarModule`, `instIsScalarTower_1`, `instSMulCommClass`, `tendsto_integral_mul_one_add_inv_smul_sq_pow`, `instIsBoundedSMul`, `instIsScalarTower`, `MeasureTheory.FiniteMeasure.testAgainstNN_smul`, `smul_apply`
`instSMulNat` 📖	CompOp	3 math math: `nsmul_apply`, `coe_zsmulRec`, `coe_nsmul`
`instSemiring` 📖	CompOp	14 math math: `RingHom.compLeftContinuousBounded_apply_apply`, `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`
`instSub` 📖	CompOp	5 math math: `integral_const_sub`, `sub_apply`, `norm_sub_nonneg`, `coe_sub`, `mkOfCompact_sub`
`instZero` 📖	CompOp	16 math math: `forall_coe_zero_iff_zero`, `coe_nsmulRec`, `mkOfCompact_zero`, `nnnorm_def`, `zero_compContinuous`, `MeasureTheory.FiniteMeasure.testAgainstNN_zero`, `norm_def`, `instIsBoundedSMul_1`, `coe_zsmulRec`, `instIsBoundedSMul`, `add_norm_nonneg`, `norm_sub_nonneg`, `coe_zero`, `apply_le_nndist_zero`, `NNReal.upper_bound`, `lintegral_le_edist_mul`
`mkOfBound` 📖	CompOp	1 math math: `mkOfBound_coe`
`mkOfCompact` 📖	CompOp	12 math math: `ContinuousMap.addEquivBoundedOfCompact_apply`, `mkOfCompact_star`, `mkOfCompact_add`, `mkOfCompact_zero`, `mkOfCompact_apply`, `ContinuousMap.equivBoundedOfCompact_apply`, `mkOfCompact_neg`, `norm_mkOfCompact`, `mkOfCompact_one`, `ContinuousMap.isometryEquivBoundedOfCompact_apply`, `mkOfCompact_sub`, `dist_mkOfCompact`
`mkOfDiscrete` 📖	CompOp	1 math math: `mkOfDiscrete_apply`
`restrict` 📖	CompOp	6 math math: `restrict_apply`, `exists_norm_eq_restrict_eq_of_closed`, `exists_forall_mem_restrict_eq_of_closed`, `coe_restrict`, `dist_extend_extend`, `exists_norm_eq_restrict_eq`
`toContinuousMap` 📖	CompOp	15 math math: `toContinuousMapLinearMap_apply`, `dist_toContinuousMap`, `toContinuousMapMonoidHom_apply`, `Lp_nnnorm_le`, `toContinuousMapAddMonoidHom_apply`, `norm_toContinuousMap_eq`, `ContinuousMap.linearIsometryBoundedOfCompact_symm_apply`, `MeasureTheory.Lp.mem_boundedContinuousFunction_iff`, `mem_Lp`, `Lp_norm_le`, `ContinuousMap.toLp_comp_toContinuousMap`, `ContinuousMap.equivBoundedOfCompact_symm_apply`, `ContinuousMap.isometryEquivBoundedOfCompact_symm_apply`, `map_bounded'`, `coe_toContinuousMap`
`toContinuousMapAddHom` 📖	CompOp	—
`toContinuousMapAddMonoidHom` 📖	CompOp	2 math math: `toContinuousMapAddMonoidHom_apply`, `ContinuousMap.addEquivBoundedOfCompact_symm_apply`
`toContinuousMapLinearMap` 📖	CompOp	1 math math: `toContinuousMapLinearMap_apply`
`toContinuousMapMonoidHom` 📖	CompOp	1 math math: `toContinuousMapMonoidHom_apply`
`«term_→ᵇ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instAdd`	—	—
`add_compContinuous` 📖	mathematical	—	`compContinuous` `BoundedContinuousFunction` `instAdd`	—	—
`bounded` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike`	—	`map_bounded'`
`coeFnAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `BoundedContinuousFunction` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `Pi.addZeroClass` `AddMonoidHom.instFunLike` `coeFnAddMonoidHom` `instFunLike`	—	—
`coeFnMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `BoundedContinuousFunction` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `Pi.mulOneClass` `MonoidHom.instFunLike` `coeFnMonoidHom` `instFunLike`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instAdd` `Pi.instAdd`	—	—
`coe_compContinuous` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `compContinuous` `ContinuousMap` `ContinuousMap.instFunLike`	—	—
`coe_mk` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `ContinuousMap.toFun`	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instMul` `Pi.instMul`	—	—
`coe_nsmul` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instSMulNat` `Pi.instSMul` `AddMonoid.toNatSMul`	—	—
`coe_nsmulRec` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoid.toNatSMul` `Pi.addMonoid`	—	`nsmulRec.eq_1` `zero_smul` `coe_zero` `nsmulRec.eq_2` `succ_nsmul` `coe_add`
`coe_one` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instOne` `Pi.instOne`	—	—
`coe_pow` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instPow` `Pi.instPow` `Monoid.toNatPow`	—	—
`coe_prod` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `Finset.prod` `instCommMonoid` `Pi.commMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`coe_restrict` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instFunLike` `restrict`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instSMul`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instSub` `Pi.instSub`	—	—
`coe_sum` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `Finset.sum` `instAddCommMonoid` `Pi.addCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`coe_toContinuousMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ContinuousMap.instFunLike` `toContinuousMap` `BoundedContinuousFunction` `instFunLike`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instZero` `Pi.instZero`	—	—
`compContinuous_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `compContinuous` `ContinuousMap` `ContinuousMap.instFunLike`	—	—
`comp_apply` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `comp`	—	—
`const_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `const`	—	—
`const_apply'` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `const`	—	—
`continuous` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike`	—	`ContinuousMap.continuous`
`continuous_coe` 📖	mathematical	—	`Continuous` `BoundedContinuousFunction` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace` `Pi.topologicalSpace` `DFunLike.coe` `instFunLike`	—	`UniformContinuous.continuous` `uniformContinuous_coe`
`continuous_comp` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`Continuous` `BoundedContinuousFunction` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace` `comp`	—	`LipschitzWith.continuous` `lipschitz_comp`
`continuous_compContinuous` 📖	mathematical	—	`Continuous` `BoundedContinuousFunction` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace` `compContinuous`	—	`LipschitzWith.continuous` `lipschitz_compContinuous`
`continuous_eval` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `DFunLike.coe`	—	`ContinuousEval.continuous_eval`
`continuous_eval_const` 📖	mathematical	—	`Continuous` `DFunLike.coe`	—	`ContinuousEvalConst.continuous_eval_const`
`dist_coe_le_dist` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instDist`	—	`le_csInf` `dist_set_exists`
`dist_eq` 📖	mathematical	—	`Dist.dist` `BoundedContinuousFunction` `instDist` `InfSet.sInf` `Real` `Real.instInfSet` `setOf` `Real.instLE` `Real.instZero`	—	—
`dist_eq_iSup` 📖	mathematical	—	`Dist.dist` `BoundedContinuousFunction` `instDist` `iSup` `Real` `Real.instSupSet` `PseudoMetricSpace.toDist` `DFunLike.coe` `instFunLike`	—	`isEmpty_or_nonempty` `iSup_of_empty'` `Real.sSup_empty` `dist_zero_of_empty` `LE.le.antisymm` `dist_le_iff_of_nonempty` `le_ciSup` `Set.forall_mem_range` `dist_set_exists` `ciSup_le` `dist_coe_le_dist`
`dist_extend_extend` 📖	mathematical	—	`Dist.dist` `BoundedContinuousFunction` `instDist` `extend` `Real` `Real.instMax` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `instTopologicalSpaceSubtype` `Set.instMembership` `restrict`	—	`le_antisymm` `dist_le` `le_max_iff` `dist_nonneg` `em` `extend_apply` `LE.le.trans` `dist_coe_le_dist` `le_max_left` `extend_apply'` `CanLift.prf` `Subtype.canLift` `le_max_right` `max_le` `Subtype.coe_prop`
`dist_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Dist.dist` `BoundedContinuousFunction` `instDist` `PseudoMetricSpace.toDist` `DFunLike.coe` `instFunLike`	—	`le_trans` `dist_coe_le_dist` `csInf_le`
`dist_le_iff_of_nonempty` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `BoundedContinuousFunction` `instDist` `PseudoMetricSpace.toDist` `DFunLike.coe` `instFunLike`	—	`le_trans` `dist_coe_le_dist` `dist_le` `dist_nonneg`
`dist_lt_iff_of_compact` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Dist.dist` `BoundedContinuousFunction` `instDist` `PseudoMetricSpace.toDist` `DFunLike.coe` `instFunLike`	—	`lt_of_le_of_lt` `dist_coe_le_dist` `dist_lt_of_nonempty_compact` `le_antisymm` `dist_eq` `csInf_le` `le_rfl`
`dist_lt_iff_of_nonempty_compact` 📖	mathematical	—	`Real` `Real.instLT` `Dist.dist` `BoundedContinuousFunction` `instDist` `PseudoMetricSpace.toDist` `DFunLike.coe` `instFunLike`	—	`lt_of_le_of_lt` `dist_coe_le_dist` `dist_lt_of_nonempty_compact`
`dist_lt_of_nonempty_compact` 📖	mathematical	`Real` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike`	`instDist`	—	`Continuous.dist` `ContinuousMapClass.map_continuous` `BoundedContinuousMapClass.toContinuousMapClass` `instBoundedContinuousMapClass` `IsCompact.exists_isMaxOn` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `isCompact_univ` `Set.univ_nonempty` `Continuous.continuousOn` `lt_of_le_of_lt` `dist_le_iff_of_nonempty`
`dist_set_exists` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike`	—	`Metric.isBounded_iff` `Bornology.IsBounded.union` `isBounded_range` `le_max_left` `LE.le.trans` `Set.mem_range_self` `le_max_right`
`dist_zero_of_empty` 📖	mathematical	—	`Dist.dist` `BoundedContinuousFunction` `instDist` `Real` `Real.instZero`	—	`ext` `dist_self`
`edist_eq_iSup` 📖	mathematical	—	`EDist.edist` `BoundedContinuousFunction` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `instPseudoMetricSpace` `iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `instFunLike`	—	`edist_nndist` `nndist_eq_iSup` `ENNReal.coe_iSup` `nndist_coe_le_nndist`
`eq_of_empty` 📖	—	—	—	—	`ext`
`evalCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `BoundedContinuousFunction` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace` `instAddCommMonoid` `instModule` `ContinuousLinearMap.funLike` `evalCLM` `instFunLike`	—	—
`ext` 📖	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike`	—	`ext`
`extend_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `extend` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`Function.Injective.extend_apply` `Function.Embedding.injective`
`extend_apply'` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	`BoundedContinuousFunction` `instFunLike` `extend`	—	`Function.extend_apply'`
`extend_comp` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `extend` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`Function.extend_comp` `Function.Embedding.injective`
`extend_of_empty` 📖	mathematical	—	`extend`	—	`DFunLike.coe_injective` `Function.extend_of_isEmpty`
`forall_coe_one_iff_one` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instOne`	—	`DFunLike.ext_iff`
`forall_coe_zero_iff_zero` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instZero`	—	`DFunLike.ext_iff`
`indicator_apply` 📖	mathematical	`IsClopen`	`DFunLike.coe` `BoundedContinuousFunction` `Real` `Real.pseudoMetricSpace` `instFunLike` `indicator` `Set.indicator` `Real.instZero` `Pi.instOne` `Real.instOne`	—	—
`instBoundedContinuousMapClass` 📖	mathematical	—	`BoundedContinuousMapClass` `BoundedContinuousFunction` `instFunLike`	—	`ContinuousMap.continuous_toFun` `map_bounded'`
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `BoundedContinuousFunction` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace`	—	`Metric.complete_of_cauchySeq_tendsto` `cauchySeq_iff_le_tendsto_0` `le_trans` `dist_coe_le_dist` `le_of_tendsto` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.dist` `tendsto_const_nhds` `Filter.eventually_atTop` `le_refl` `Metric.tendstoUniformly_iff` `Filter.Eventually.mono` `tendsto_order` `dist_comm` `lt_of_le_of_lt` `TendstoUniformly.continuous` `Filter.Frequently.of_forall` `continuous` `bounded` `dist_triangle4_left` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `tendsto_iff_dist_tendsto_zero` `squeeze_zero` `dist_nonneg` `dist_le` `cauchySeq_tendsto_of_complete`
`instContinuousEval` 📖	mathematical	—	`ContinuousEval` `BoundedContinuousFunction` `instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace`	—	`continuous_prod_of_continuous_lipschitzWith` `continuous` `lipschitz_eval_const`
`instContinuousEvalConst` 📖	mathematical	—	`ContinuousEvalConst` `BoundedContinuousFunction` `instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace`	—	`ContinuousEval.toContinuousEvalConst` `instContinuousEval`
`instIsBoundedSMul` 📖	mathematical	—	`IsBoundedSMul` `BoundedContinuousFunction` `instPseudoMetricSpace` `instZero` `instSMul`	—	`dist_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `dist_nonneg` `LE.le.trans` `dist_smul_pair` `mul_le_mul_of_nonneg_left` `dist_coe_le_dist` `dist_pair_smul`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `BoundedContinuousFunction` `instSMul` `MulOpposite` `MulOpposite.instPseudoMetricSpace` `MulOpposite.instZero` `IsBoundedSMul.op`	—	`IsBoundedSMul.op` `ext` `IsCentralScalar.op_smul_eq_smul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `BoundedContinuousFunction` `instSMul`	—	`ext` `smul_assoc`
`instLipschitzAdd` 📖	mathematical	—	`LipschitzAdd` `BoundedContinuousFunction` `instPseudoMetricSpace` `instAddMonoid` `instBoundedAddOfLipschitzAdd` `LipschitzAdd.continuousAdd`	—	`instBoundedAddOfLipschitzAdd` `LipschitzAdd.continuousAdd` `NNReal.coe_nonneg` `lipschitzWith_iff_dist_le_mul` `dist_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `dist_nonneg` `le_trans` `lipschitz_with_lipschitz_const_add` `mul_le_mul_of_nonneg_left` `max_le_max` `dist_coe_le_dist`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `BoundedContinuousFunction` `instSMul`	—	`ext` `SMulCommClass.smul_comm`
`intCast_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instIntCast`	—	—
`isBounded_image` 📖	mathematical	—	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `Set.image` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike`	—	`Bornology.IsBounded.subset` `isBounded_range` `Set.image_subset_range`
`isBounded_range` 📖	mathematical	—	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `Set.range` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike`	—	`Metric.isBounded_range_iff` `bounded`
`isEmbedding_coeFn` 📖	mathematical	—	`Topology.IsEmbedding` `BoundedContinuousFunction` `UniformFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace` `UniformFun.topologicalSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniformFun.ofFun` `instFunLike`	—	`isInducing_coeFn` `ext`
`isInducing_coeFn` 📖	mathematical	—	`Topology.IsInducing` `BoundedContinuousFunction` `UniformFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace` `UniformFun.topologicalSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniformFun.ofFun` `instFunLike`	—	`Topology.isInducing_iff_nhds` `eq_of_forall_le_iff` `Filter.tendsto_iff_comap` `Filter.tendsto_id'` `tendsto_iff_tendstoUniformly` `UniformFun.tendsto_iff_tendstoUniformly`
`isometry_extend` 📖	mathematical	—	`Isometry` `BoundedContinuousFunction` `PseudoMetricSpace.toPseudoEMetricSpace` `instPseudoMetricSpace` `extend`	—	`Isometry.of_dist_eq` `dist_extend_extend` `dist_self` `sup_of_le_left`
`lipschitz_comp` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`BoundedContinuousFunction` `instPseudoMetricSpace` `comp`	—	`LipschitzWith.of_dist_le_mul` `dist_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `dist_nonneg` `LipschitzWith.dist_le_mul` `mul_le_mul_of_nonneg_left` `dist_coe_le_dist` `NNReal.coe_nonneg`
`lipschitz_compContinuous` 📖	mathematical	—	`LipschitzWith` `BoundedContinuousFunction` `PseudoMetricSpace.toPseudoEMetricSpace` `instPseudoMetricSpace` `NNReal` `instOneNNReal` `compContinuous`	—	`LipschitzWith.mk_one` `dist_le` `dist_nonneg` `dist_coe_le_dist`
`lipschitz_eval_const` 📖	mathematical	—	`LipschitzWith` `BoundedContinuousFunction` `PseudoMetricSpace.toPseudoEMetricSpace` `instPseudoMetricSpace` `NNReal` `instOneNNReal` `DFunLike.coe` `instFunLike`	—	`LipschitzWith.mk_one` `dist_coe_le_dist`
`lipschitz_evalx` 📖	mathematical	—	`LipschitzWith` `BoundedContinuousFunction` `PseudoMetricSpace.toPseudoEMetricSpace` `instPseudoMetricSpace` `NNReal` `instOneNNReal` `DFunLike.coe` `instFunLike`	—	`lipschitz_eval_const`
`map_bounded'` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `ContinuousMap.toFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `toContinuousMap`	—	—
`mkOfBound_coe` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ContinuousMap.instFunLike`	`BoundedContinuousFunction` `instFunLike` `mkOfBound`	—	—
`mkOfCompact_add` 📖	mathematical	—	`mkOfCompact` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ContinuousMap.instAdd` `BoundedContinuousFunction` `instAdd`	—	—
`mkOfCompact_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `mkOfCompact` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ContinuousMap.instFunLike`	—	—
`mkOfCompact_one` 📖	mathematical	—	`mkOfCompact` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ContinuousMap.instOne` `BoundedContinuousFunction` `instOne`	—	—
`mkOfCompact_zero` 📖	mathematical	—	`mkOfCompact` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ContinuousMap.instZero` `BoundedContinuousFunction` `instZero`	—	—
`mkOfDiscrete_apply` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `mkOfDiscrete`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instMul`	—	—
`natCast_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instNatCast`	—	—
`nndist_coe_le_nndist` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instPseudoMetricSpace`	—	`dist_coe_le_dist`
`nndist_eq` 📖	mathematical	—	`NNDist.nndist` `BoundedContinuousFunction` `PseudoMetricSpace.toNNDist` `instPseudoMetricSpace` `InfSet.sInf` `NNReal` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `NNReal.instConditionallyCompleteLinearOrderBot` `setOf`	—	`dist_eq` `NNReal.val_eq_coe` `NNReal.coe_sInf` `NNReal.coe_image`
`nndist_eq_iSup` 📖	mathematical	—	`NNDist.nndist` `BoundedContinuousFunction` `PseudoMetricSpace.toNNDist` `instPseudoMetricSpace` `iSup` `NNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `NNReal.instConditionallyCompleteLinearOrderBot` `DFunLike.coe` `instFunLike`	—	`dist_eq_iSup` `NNReal.coe_iSup`
`nndist_set_exists` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike`	—	`dist_set_exists`
`nsmul_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instSMulNat` `AddMonoid.toNatSMul`	—	—
`one_compContinuous` 📖	mathematical	—	`compContinuous` `BoundedContinuousFunction` `instOne`	—	—
`pow_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instPow` `Monoid.toNatPow`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `Finset.prod` `instCommMonoid`	—	`coe_prod` `Finset.prod_apply`
`restrict_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instFunLike` `restrict`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instSMul`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `instSub`	—	—
`sum_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `Finset.sum` `instAddCommMonoid`	—	`coe_sum` `Finset.sum_apply`
`tendsto_iff_tendstoUniformly` 📖	mathematical	—	`Filter.Tendsto` `BoundedContinuousFunction` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace` `TendstoUniformly` `DFunLike.coe` `instFunLike`	—	`Metric.tendstoUniformly_iff` `Filter.Eventually.mp` `Metric.tendsto_nhds` `Filter.Eventually.of_forall` `lt_of_le_of_lt` `dist_coe_le_dist` `dist_comm` `Nat.instAtLeastTwoHAddOfNat` `Metric.dist_mem_uniformity` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `dist_le` `LT.lt.le` `le_of_lt` `half_lt_self`
`toContinuousMapAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `BoundedContinuousFunction` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `ContinuousMap.instAddZeroClassOfContinuousAdd` `AddMonoidHom.instFunLike` `toContinuousMapAddMonoidHom` `toContinuousMap`	—	—
`toContinuousMapLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `BoundedContinuousFunction` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instAddCommMonoid` `ContinuousMap.instAddCommMonoidOfContinuousAdd` `instModule` `ContinuousMap.module` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.instFunLike` `toContinuousMapLinearMap` `toContinuousMap`	—	`UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul`
`toContinuousMapMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `BoundedContinuousFunction` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `ContinuousMap.instMulOneClassOfContinuousMul` `MonoidHom.instFunLike` `toContinuousMapMonoidHom` `toContinuousMap`	—	—
`uniformContinuous_coe` 📖	mathematical	—	`UniformContinuous` `BoundedContinuousFunction` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace` `Pi.uniformSpace` `DFunLike.coe` `instFunLike`	—	`uniformContinuous_pi` `LipschitzWith.uniformContinuous` `lipschitz_eval_const`
`uniformContinuous_comp` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`UniformContinuous` `BoundedContinuousFunction` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace` `comp`	—	`LipschitzWith.uniformContinuous` `lipschitz_comp`
`zero_compContinuous` 📖	mathematical	—	`compContinuous` `BoundedContinuousFunction` `instZero`	—	—

BoundedContinuousFunction.NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`upper_bound` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `BoundedContinuousFunction.instPseudoMetricSpace` `BoundedContinuousFunction.instZero` `instZeroNNReal`	—	`BoundedContinuousFunction.dist_coe_le_dist` `NNReal.nndist_zero_eq_val'`

BoundedContinuousFunction.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—

BoundedContinuousMapClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_bounded` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe`	—	—
`toContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	—

MonoidHom

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLeftContinuousBounded_apply` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike`	`BoundedContinuousFunction` `BoundedContinuousFunction.instMulOneClass` `compLeftContinuousBounded` `BoundedContinuousFunction.comp`	—	—

(root)

Definitions

Name	Category	Theorems
`BoundedContinuousMapClass` 📖	CompData	5 math math: `TestFunctionClass.instBoundedContinuousMapClass`, `SchwartzMap.instBoundedContinuousMapClass`, `ZeroAtInftyContinuousMap.instBoundedContinuousMapClass`, `ContDiffMapSupportedInClass.instBoundedContinuousMapClass`, `BoundedContinuousFunction.instBoundedContinuousMapClass`

---

← Back to Index