ContinuousMapZero

📁 Source: Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

Statistics

Metric	Count
Definitions `ContinuousMapZero`, `coeFnAddMonoidHom`, `comp`, `evalCLM`, `id`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instFunLike`, `instMetricSpace`, `instModule`, `instMul`, `instNeg`, `instNonUnitalCommRing`, `instNonUnitalCommSemiring`, `instNonUnitalNormedCommRing`, `instNorm`, `instNormedAddCommGroup`, `instNormedSpaceOfNormedAlgebra`, `instPartialOrder`, `instSMul`, `instStarRing`, `instSub`, `instTopologicalSpace`, `instUniformSpace`, `instZero`, `mkD`, `nonUnitalStarAlgHom_postcomp`, `nonUnitalStarAlgHom_precomp`, `toContinuousMap`, `toContinuousMapCLM`, `toContinuousMapHom`, `«termC(_,_)₀»`₀»), `zeroOfFactMem`, `arrowCongrLeft₀`	35
Theorems `coeFnAddMonoidHom_apply`, `coe_add`, `coe_mk`, `coe_mul`, `coe_neg`, `coe_smul`, `coe_star`, `coe_sub`, `coe_sum`, `coe_toContinuousMapHom`, `coe_zero`, `comp_apply`, `continuous_comp_left`, `continuous_postcomp`, `continuous_precomp`, `evalCLM_apply`, `ext`, `ext_iff`, `id_toFun`, `instCStarRing`, `instCanLift`, `instCompleteSpaceOfT1SpaceOfContinuousMap`, `instContinuousEval`, `instContinuousEvalConst`, `instContinuousMapClass`, `instContinuousNeg`, `instIsScalarTower`, `instIsScalarTower'`, `instR0Space`, `instR1Space`, `instRegularSpace`, `instSMulCommClass`, `instSMulCommClass'`, `instStarModule`, `instT0Space`, `instT1Space`, `instT2Space`, `instT3Space`, `instTrivialStar`, `instZeroHomClass`, `isClosedEmbedding_toContinuousMap`, `isEmbedding_toContinuousMap`, `isUniformEmbedding_comp`, `isUniformEmbedding_toContinuousMap`, `isometry_toContinuousMap`, `le_def`, `map_zero'`, `mkD_apply_of_continuous`, `mkD_apply_of_continuousOn`, `mkD_eq_mkD_of_map_zero`, `mkD_eq_self`, `mkD_of_continuous`, `mkD_of_continuousOn`, `mkD_of_not_continuous`, `mkD_of_not_continuousOn`, `mkD_of_not_zero`, `nonUnitalStarAlgHom_postcomp_apply`, `nonUnitalStarAlgHom_precomp_apply`, `norm_def`, `postcomp_injective`, `range_toContinuousMap`, `toContinuousMapCLM_apply`, `toContinuousMapHom_apply`, `toContinuousMap_id`, `toContinuousMap_injective`	65
Total	100

ContinuousMapZero

Definitions

Name	Category	Theorems
`coeFnAddMonoidHom` 📖	CompOp	1 math math: `coeFnAddMonoidHom_apply`
`comp` 📖	CompOp	12 math math: `postcomp_injective`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal`, `cfcₙHom_comp`, `nonUnitalStarAlgHom_precomp_apply`, `continuous_comp_left`, `continuous_postcomp`, `isUniformEmbedding_comp`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `continuous_precomp`, `comp_apply`, `nonUnitalStarAlgHom_postcomp_apply`, `cfcₙHomSuperset_apply`
`evalCLM` 📖	CompOp	1 math math: `evalCLM_apply`
`id` 📖	CompOp	8 math math: `toContinuousMap_id`, `id_toFun`, `QuasispectrumRestricts.nonUnitalStarAlgHom_id`, `cfcₙHom_id`, `cfcₙAux_id`, `cfcₙHomSuperset_id`, `elemental_eq_top`, `adjoin_id_dense`
`instAdd` 📖	CompOp	3 math math: `coe_add`, `toNNReal_mul_add_neg_mul_add_mul_neg_eq`, `toNNReal_add_add_neg_add_neg_eq`
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	72 math math: `cfcₙ_def`, `continuous_cfcₙHomSuperset_left`, `cfcₙL_integral`, `norm_cfcₙHom`, `cfcₙHom_mono`, `NonUnitalIsometricContinuousFunctionalCalculus.isometric`, `cfcₙHom_apply_mem_elemental`, `cfcₙHom_of_cfcHom_injective`, `isClosedEmbedding_cfcₙAux`, `QuasispectrumRestricts.nonUnitalStarAlgHom_id`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal`, `cfcₙHom_mem_elemental`, `cfcₙ_eq_cfcₙL_mkD`, `cfcₙ_apply_mkD`, `cfcₙHom_id`, `inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux`, `range_cfcₙHom`, `NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding`, `cfcₙHom_integral`, `cfcₙAux_id`, `isometry_cfcₙHom`, `cfcₙHom_predicate`, `cfcₙHom_comp`, `Commute.cfcₙHom`, `QuasispectrumRestricts.continuous_nonUnitalStarAlgHom`, `toContinuousMapCLM_apply`, `range_cfcₙ_eq_range_cfcₙHom`, `range_cfcₙHom_le`, `nonUnitalStarAlgHom_precomp_apply`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `cfcₙHom_isClosedEmbedding`, `cfcₙHom_le_iff`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply`, `mul_nonUnitalStarAlgHom_apply_eq_zero`, `cfcₙHom_eq_cfcₙ_extend`, `cfcₙAux_injective`, `QuasispectrumRestricts.nonUnitalStarAlgHom_injective`, `toContinuousMapHom_toNNReal`, `cfcₙHom_map_quasispectrum`, `QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom`, `spec_cfcₙAux`, `cfcₙHom_injective`, `cfcₙHomSuperset_id`, `evalCLM_apply`, `instSMulCommClass'`, `nnnorm_cfcₙHom`, `continuous_cfcₙHom_of_cfcHom`, `isClosedEmbedding_cfcₙHom_of_cfcHom`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective`, `IsSelfAdjoint.commute_cfcₙHom`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate`, `coe_sum`, `toContinuousMapHom_apply`, `cfcₙAux_mem_range_inr`, `cfcₙHom_continuous`, `cfcₙHomSuperset_continuous`, `cfcₙ_apply_pi`, `continuous_cfcₙAux`, `cfcₙ_eq_cfcₙL`, `cfcₙL_apply`, `nonUnitalStarAlgHom_postcomp_apply`, `instIsScalarTower'`, `cfcₙL_integrable`, `cfcₙHom_of_cfcHom_map_quasispectrum`, `cfcₙHomSuperset_apply`, `cfcₙ_apply`, `coe_toContinuousMapHom`, `cfcₙHom_nonneg_iff`, `nonUnitalStarAlgHom_apply_mul_eq_zero`, `coeFnAddMonoidHom_apply`, `NonUnitalStarAlgHom.continuous_realContinuousMapZeroOfNNReal`
`instFunLike` 📖	CompOp	41 math math: `coe_star`, `instContinuousEval`, `isEmbedding_toContinuousMap`, `toContinuousMap_id`, `id_toFun`, `instCanLift`, `coe_mul`, `coe_add`, `ext_iff`, `integral_apply`, `coe_mk`, `toContinuousMapCLM_apply`, `coe_neg`, `coe_smul`, `instContinuousEvalConst`, `norm_def`, `cfcₙHom_eq_cfcₙ_extend`, `mkD_eq_self`, `cfcₙHom_map_quasispectrum`, `spec_cfcₙAux`, `evalCLM_apply`, `instContinuousMapClass`, `le_def`, `NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate`, `coe_sum`, `toContinuousMapHom_apply`, `coe_sub`, `isUniformEmbedding_toContinuousMap`, `mkD_apply_of_continuous`, `mkD_eq_mkD_of_map_zero`, `comp_apply`, `mkD_apply_of_continuousOn`, `toContinuousMap_injective`, `cfcₙHom_of_cfcHom_map_quasispectrum`, `coe_toContinuousMapHom`, `instZeroHomClass`, `toNNReal_apply`, `coeFnAddMonoidHom_apply`, `isClosedEmbedding_toContinuousMap`, `range_toContinuousMap`, `coe_zero`
`instMetricSpace` 📖	CompOp	3 math math: `NonUnitalIsometricContinuousFunctionalCalculus.isometric`, `isometry_toContinuousMap`, `isometry_cfcₙHom`
`instModule` 📖	CompOp	70 math math: `cfcₙ_def`, `continuous_cfcₙHomSuperset_left`, `cfcₙL_integral`, `norm_cfcₙHom`, `cfcₙHom_mono`, `NonUnitalIsometricContinuousFunctionalCalculus.isometric`, `cfcₙHom_apply_mem_elemental`, `cfcₙHom_of_cfcHom_injective`, `isClosedEmbedding_cfcₙAux`, `QuasispectrumRestricts.nonUnitalStarAlgHom_id`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal`, `cfcₙHom_mem_elemental`, `cfcₙ_eq_cfcₙL_mkD`, `cfcₙ_apply_mkD`, `cfcₙHom_id`, `inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux`, `range_cfcₙHom`, `NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding`, `cfcₙHom_integral`, `cfcₙAux_id`, `isometry_cfcₙHom`, `cfcₙHom_predicate`, `cfcₙHom_comp`, `Commute.cfcₙHom`, `QuasispectrumRestricts.continuous_nonUnitalStarAlgHom`, `toContinuousMapCLM_apply`, `range_cfcₙ_eq_range_cfcₙHom`, `range_cfcₙHom_le`, `nonUnitalStarAlgHom_precomp_apply`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `cfcₙHom_isClosedEmbedding`, `cfcₙHom_le_iff`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply`, `mul_nonUnitalStarAlgHom_apply_eq_zero`, `cfcₙHom_eq_cfcₙ_extend`, `cfcₙAux_injective`, `QuasispectrumRestricts.nonUnitalStarAlgHom_injective`, `toContinuousMapHom_toNNReal`, `cfcₙHom_map_quasispectrum`, `QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom`, `spec_cfcₙAux`, `cfcₙHom_injective`, `cfcₙHomSuperset_id`, `evalCLM_apply`, `nnnorm_cfcₙHom`, `continuous_cfcₙHom_of_cfcHom`, `isClosedEmbedding_cfcₙHom_of_cfcHom`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective`, `IsSelfAdjoint.commute_cfcₙHom`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate`, `toContinuousMapHom_apply`, `cfcₙAux_mem_range_inr`, `cfcₙHom_continuous`, `cfcₙHomSuperset_continuous`, `cfcₙ_apply_pi`, `continuous_cfcₙAux`, `cfcₙ_eq_cfcₙL`, `cfcₙL_apply`, `nonUnitalStarAlgHom_postcomp_apply`, `elemental_eq_top`, `adjoin_id_dense`, `cfcₙL_integrable`, `cfcₙHom_of_cfcHom_map_quasispectrum`, `cfcₙHomSuperset_apply`, `cfcₙ_apply`, `coe_toContinuousMapHom`, `cfcₙHom_nonneg_iff`, `nonUnitalStarAlgHom_apply_mul_eq_zero`, `NonUnitalStarAlgHom.continuous_realContinuousMapZeroOfNNReal`
`instMul` 📖	CompOp	2 math math: `coe_mul`, `toNNReal_mul_add_neg_mul_add_mul_neg_eq`
`instNeg` 📖	CompOp	6 math math: `coe_neg`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply`, `toNNReal_mul_add_neg_mul_add_mul_neg_eq`, `instContinuousNeg`, `toNNReal_add_add_neg_add_neg_eq`, `toNNReal_neg_smul`
`instNonUnitalCommRing` 📖	CompOp	14 math math: `isClosedEmbedding_cfcₙAux`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal`, `cfcₙAux_id`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply`, `mul_nonUnitalStarAlgHom_apply_eq_zero`, `cfcₙAux_injective`, `spec_cfcₙAux`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `cfcₙAux_mem_range_inr`, `continuous_cfcₙAux`, `elemental_eq_top`, `nonUnitalStarAlgHom_apply_mul_eq_zero`, `NonUnitalStarAlgHom.continuous_realContinuousMapZeroOfNNReal`
`instNonUnitalCommSemiring` 📖	CompOp	61 math math: `coe_star`, `cfcₙ_def`, `continuous_cfcₙHomSuperset_left`, `norm_cfcₙHom`, `cfcₙHom_mono`, `NonUnitalIsometricContinuousFunctionalCalculus.isometric`, `cfcₙHom_apply_mem_elemental`, `cfcₙHom_of_cfcHom_injective`, `QuasispectrumRestricts.nonUnitalStarAlgHom_id`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal`, `cfcₙHom_mem_elemental`, `cfcₙ_apply_mkD`, `cfcₙHom_id`, `inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux`, `range_cfcₙHom`, `NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding`, `instStarOrderedRing`, `cfcₙHom_integral`, `isometry_cfcₙHom`, `cfcₙHom_predicate`, `cfcₙHom_comp`, `Commute.cfcₙHom`, `QuasispectrumRestricts.continuous_nonUnitalStarAlgHom`, `range_cfcₙ_eq_range_cfcₙHom`, `range_cfcₙHom_le`, `nonUnitalStarAlgHom_precomp_apply`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `cfcₙHom_isClosedEmbedding`, `cfcₙHom_le_iff`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply`, `cfcₙHom_eq_cfcₙ_extend`, `QuasispectrumRestricts.nonUnitalStarAlgHom_injective`, `instTrivialStar`, `toContinuousMapHom_toNNReal`, `cfcₙHom_map_quasispectrum`, `QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom`, `cfcₙHom_injective`, `cfcₙHomSuperset_id`, `instSMulCommClass'`, `nnnorm_cfcₙHom`, `continuous_cfcₙHom_of_cfcHom`, `isClosedEmbedding_cfcₙHom_of_cfcHom`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective`, `IsSelfAdjoint.commute_cfcₙHom`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate`, `toContinuousMapHom_apply`, `cfcₙHom_continuous`, `cfcₙHomSuperset_continuous`, `cfcₙ_apply_pi`, `cfcₙL_apply`, `nonUnitalStarAlgHom_postcomp_apply`, `elemental_eq_top`, `adjoin_id_dense`, `instIsScalarTower'`, `cfcₙHom_of_cfcHom_map_quasispectrum`, `instStarModule`, `cfcₙHomSuperset_apply`, `cfcₙ_apply`, `coe_toContinuousMapHom`, `cfcₙHom_nonneg_iff`
`instNonUnitalNormedCommRing` 📖	CompOp	3 math math: `nnnorm_cfcₙHom`, `instCStarRing`, `elemental_eq_top`
`instNorm` 📖	CompOp	2 math math: `norm_cfcₙHom`, `norm_def`
`instNormedAddCommGroup` 📖	CompOp	6 math math: `cfcₙL_integral`, `hasFiniteIntegral_of_bound`, `cfcₙHom_integral`, `integral_apply`, `hasFiniteIntegral_mkD_restrict_of_bound`, `hasFiniteIntegral_mkD_of_bound`
`instNormedSpaceOfNormedAlgebra` 📖	CompOp	4 math math: `cfcₙL_integral`, `cfcₙHom_integral`, `integral_apply`, `elemental_eq_top`
`instPartialOrder` 📖	CompOp	4 math math: `instStarOrderedRing`, `cfcₙHom_le_iff`, `le_def`, `cfcₙHom_nonneg_iff`
`instSMul` 📖	CompOp	8 math math: `instSMulCommClass`, `instIsScalarTower`, `coe_smul`, `instSMulCommClass'`, `toNNReal_neg_smul`, `toNNReal_smul`, `instIsScalarTower'`, `instStarModule`
`instStarRing` 📖	CompOp	69 math math: `coe_star`, `cfcₙ_def`, `continuous_cfcₙHomSuperset_left`, `norm_cfcₙHom`, `cfcₙHom_mono`, `NonUnitalIsometricContinuousFunctionalCalculus.isometric`, `cfcₙHom_apply_mem_elemental`, `cfcₙHom_of_cfcHom_injective`, `isClosedEmbedding_cfcₙAux`, `QuasispectrumRestricts.nonUnitalStarAlgHom_id`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal`, `cfcₙHom_mem_elemental`, `cfcₙ_apply_mkD`, `cfcₙHom_id`, `inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux`, `range_cfcₙHom`, `NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding`, `instStarOrderedRing`, `cfcₙHom_integral`, `cfcₙAux_id`, `isometry_cfcₙHom`, `cfcₙHom_predicate`, `cfcₙHom_comp`, `Commute.cfcₙHom`, `QuasispectrumRestricts.continuous_nonUnitalStarAlgHom`, `range_cfcₙ_eq_range_cfcₙHom`, `range_cfcₙHom_le`, `nonUnitalStarAlgHom_precomp_apply`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `cfcₙHom_isClosedEmbedding`, `cfcₙHom_le_iff`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply`, `mul_nonUnitalStarAlgHom_apply_eq_zero`, `cfcₙHom_eq_cfcₙ_extend`, `cfcₙAux_injective`, `QuasispectrumRestricts.nonUnitalStarAlgHom_injective`, `instTrivialStar`, `toContinuousMapHom_toNNReal`, `cfcₙHom_map_quasispectrum`, `QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom`, `spec_cfcₙAux`, `cfcₙHom_injective`, `cfcₙHomSuperset_id`, `nnnorm_cfcₙHom`, `continuous_cfcₙHom_of_cfcHom`, `isClosedEmbedding_cfcₙHom_of_cfcHom`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective`, `IsSelfAdjoint.commute_cfcₙHom`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate`, `toContinuousMapHom_apply`, `cfcₙAux_mem_range_inr`, `instCStarRing`, `cfcₙHom_continuous`, `cfcₙHomSuperset_continuous`, `cfcₙ_apply_pi`, `continuous_cfcₙAux`, `cfcₙL_apply`, `nonUnitalStarAlgHom_postcomp_apply`, `elemental_eq_top`, `adjoin_id_dense`, `cfcₙHom_of_cfcHom_map_quasispectrum`, `instStarModule`, `cfcₙHomSuperset_apply`, `cfcₙ_apply`, `coe_toContinuousMapHom`, `cfcₙHom_nonneg_iff`, `nonUnitalStarAlgHom_apply_mul_eq_zero`, `NonUnitalStarAlgHom.continuous_realContinuousMapZeroOfNNReal`
`instSub` 📖	CompOp	1 math math: `coe_sub`
`instTopologicalSpace` 📖	CompOp	41 math math: `cfcₙL_integral`, `instContinuousEval`, `isEmbedding_toContinuousMap`, `isClosedEmbedding_cfcₙAux`, `aeStronglyMeasurable_mkD_of_uncurry`, `cfcₙ_eq_cfcₙL_mkD`, `NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding`, `instT0Space`, `QuasispectrumRestricts.continuous_nonUnitalStarAlgHom`, `toContinuousMapCLM_apply`, `instT1Space`, `continuous_comp_left`, `cfcₙHom_isClosedEmbedding`, `instContinuousEvalConst`, `continuous_postcomp`, `instR0Space`, `QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom`, `instContinuousNeg`, `evalCLM_apply`, `continuous_cfcₙHom_of_cfcHom`, `isClosedEmbedding_cfcₙHom_of_cfcHom`, `aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry`, `NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate`, `instT2Space`, `cfcₙHom_continuous`, `cfcₙHomSuperset_continuous`, `aeStronglyMeasurable_mkD_restrict_of_uncurry`, `instRegularSpace`, `continuous_precomp`, `continuous_cfcₙAux`, `cfcₙ_eq_cfcₙL`, `cfcₙL_apply`, `aeStronglyMeasurable_restrict_mkD_of_uncurry`, `elemental_eq_top`, `adjoin_id_dense`, `instR1Space`, `instT3Space`, `cfcₙL_integrable`, `continuous_toNNReal`, `NonUnitalStarAlgHom.continuous_realContinuousMapZeroOfNNReal`, `isClosedEmbedding_toContinuousMap`
`instUniformSpace` 📖	CompOp	4 math math: `instCompleteSpaceOfT1SpaceOfContinuousMap`, `isUniformEmbedding_comp`, `isUniformEmbedding_toContinuousMap`, `elemental_eq_top`
`instZero` 📖	CompOp	5 math math: `cfcₙ_eq_cfcₙL_mkD`, `cfcₙ_apply_mkD`, `elemental_eq_top`, `cfcₙHom_nonneg_iff`, `coe_zero`
`mkD` 📖	CompOp	17 math math: `aeStronglyMeasurable_mkD_of_uncurry`, `cfcₙ_eq_cfcₙL_mkD`, `cfcₙ_apply_mkD`, `mkD_of_not_zero`, `mkD_eq_self`, `aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry`, `mkD_of_not_continuous`, `hasFiniteIntegral_mkD_restrict_of_bound`, `mkD_of_continuous`, `mkD_apply_of_continuous`, `mkD_of_not_continuousOn`, `mkD_eq_mkD_of_map_zero`, `aeStronglyMeasurable_mkD_restrict_of_uncurry`, `mkD_of_continuousOn`, `aeStronglyMeasurable_restrict_mkD_of_uncurry`, `mkD_apply_of_continuousOn`, `hasFiniteIntegral_mkD_of_bound`
`nonUnitalStarAlgHom_postcomp` 📖	CompOp	1 math math: `nonUnitalStarAlgHom_postcomp_apply`
`nonUnitalStarAlgHom_precomp` 📖	CompOp	1 math math: `nonUnitalStarAlgHom_precomp_apply`
`toContinuousMap` 📖	CompOp	2 math math: `isometry_toContinuousMap`, `map_zero'`
`toContinuousMapCLM` 📖	CompOp	1 math math: `toContinuousMapCLM_apply`
`toContinuousMapHom` 📖	CompOp	3 math math: `toContinuousMapHom_toNNReal`, `toContinuousMapHom_apply`, `coe_toContinuousMapHom`
`«termC(_,_)₀»` 📖₀» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFnAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `Pi.addZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidHom.instFunLike` `coeFnAddMonoidHom` `instFunLike`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring`
`coe_add` 📖	mathematical	—	`DFunLike.coe` `ContinuousMapZero` `AddZero.toZero` `AddZeroClass.toAddZero` `instFunLike` `instAdd` `Pi.instAdd` `AddZero.toAdd`	—	—
`coe_mk` 📖	mathematical	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`DFunLike.coe` `ContinuousMapZero` `instFunLike` `ContinuousMap` `ContinuousMap.instFunLike`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `ContinuousMapZero` `MulZeroClass.toZero` `instFunLike` `instMul` `Pi.instMul` `MulZeroClass.toMul`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `ContinuousMapZero` `NegZeroClass.toZero` `instFunLike` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `ContinuousMapZero` `instFunLike` `instSMul` `Function.hasSMul` `SMulZeroClass.toSMul`	—	—
`coe_star` 📖	mathematical	—	`DFunLike.coe` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instNonUnitalCommSemiring` `StarRing.toStarAddMonoid` `instStarRing` `Pi.instStarForall`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `ContinuousMapZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `instFunLike` `instSub` `Pi.instSub` `SubNegMonoid.toSub` `SubNegZeroMonoid.toSubNegMonoid`	—	—
`coe_sum` 📖	mathematical	—	`DFunLike.coe` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `Finset.sum` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `Pi.addCommMonoid`	—	`map_sum` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `AddMonoidHom.instAddMonoidHomClass`
`coe_toContinuousMapHom` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ContinuousMap` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instNonUnitalCommSemiring` `Module.toDistribMulAction` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `instStarRing` `ContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring` `ContinuousMap.instDistribMulActionOfContinuousConstSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `ContinuousMap.instStar` `NonUnitalStarAlgHom.instFunLike` `toContinuousMapHom` `toContinuousMap` `instFunLike` `instContinuousMapClass`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `ContinuousMapZero` `instFunLike` `instZero` `Pi.instZero`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMapZero` `instFunLike` `comp`	—	—
`continuous_comp_left` 📖	mathematical	—	`Continuous` `ContinuousMapZero` `instTopologicalSpace` `comp`	—	`continuous_precomp`
`continuous_postcomp` 📖	mathematical	—	`Continuous` `ContinuousMapZero` `instTopologicalSpace` `comp`	—	`instContinuousMapClass` `Topology.IsEmbedding.continuous_iff` `isEmbedding_toContinuousMap` `Continuous.comp` `ContinuousMap.continuous_postcomp` `Topology.IsEmbedding.continuous`
`continuous_precomp` 📖	mathematical	—	`Continuous` `ContinuousMapZero` `instTopologicalSpace` `comp`	—	`instContinuousMapClass` `continuous_induced_rng` `Continuous.comp'` `ContinuousMap.continuous_precomp` `continuous_induced_dom`
`evalCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommSemiring.toSemiring` `instTopologicalSpace` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `instModule` `ContinuousLinearMap.funLike` `evalCLM` `instFunLike`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring`
`ext` 📖	—	`DFunLike.coe` `ContinuousMapZero` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousMapZero` `instFunLike`	—	`ext`
`id_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMapZero` `Set.Elem` `Set.zeroOfFactMem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instFunLike` `id`	—	—
`instCStarRing` 📖	mathematical	—	`CStarRing` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `instNonUnitalNormedCommRing` `instStarRing` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedStarGroup.to_continuousStar` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `StarRing.toStarAddMonoid` `CStarRing.to_normedStarGroup`	—	`IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `NormedStarGroup.to_continuousStar` `CStarRing.to_normedStarGroup` `CStarRing.norm_mul_self_le` `ContinuousMap.instCStarRing` `instContinuousMapClass`
`instCanLift` 📖	mathematical	—	`CanLift` `ContinuousMap` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `toContinuousMap` `instFunLike` `instContinuousMapClass` `DFunLike.coe` `ContinuousMap.instFunLike`	—	`instContinuousMapClass`
`instCompleteSpaceOfT1SpaceOfContinuousMap` 📖	mathematical	—	`CompleteSpace` `ContinuousMapZero` `UniformSpace.toTopologicalSpace` `instUniformSpace`	—	`instContinuousMapClass` `completeSpace_iff_isComplete_range` `IsUniformEmbedding.isUniformInducing` `isUniformEmbedding_toContinuousMap` `IsClosed.isComplete` `Topology.IsClosedEmbedding.isClosed_range` `isClosedEmbedding_toContinuousMap`
`instContinuousEval` 📖	mathematical	—	`ContinuousEval` `ContinuousMapZero` `instFunLike` `instTopologicalSpace`	—	`ContinuousEval.of_continuous_forget` `ContinuousMap.instContinuousEvalOfLocallyCompactPair` `instContinuousMapClass` `Topology.IsEmbedding.continuous` `isEmbedding_toContinuousMap`
`instContinuousEvalConst` 📖	mathematical	—	`ContinuousEvalConst` `ContinuousMapZero` `instFunLike` `instTopologicalSpace`	—	`ContinuousEvalConst.of_continuous_forget` `ContinuousMap.instContinuousEvalConst` `instContinuousMapClass` `Topology.IsEmbedding.continuous` `isEmbedding_toContinuousMap`
`instContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass` `ContinuousMapZero` `instFunLike`	—	`ContinuousMap.continuous`
`instContinuousNeg` 📖	mathematical	—	`ContinuousNeg` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instTopologicalSpace` `instNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing`	—	`IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing` `instContinuousMapClass` `continuous_induced_rng` `Continuous.comp` `ContinuousNeg.continuous_neg` `IsTopologicalAddGroup.toContinuousNeg` `IsSemitopologicalRing.toIsTopologicalAddGroup` `ContinuousMap.instIsTopologicalAddGroup` `continuous_induced_dom`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `ContinuousMapZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instSMul`	—	`ext` `smul_assoc` `instContinuousMapClass`
`instIsScalarTower'` 📖	mathematical	—	`IsScalarTower` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instNonUnitalCommSemiring`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `ext` `smul_assoc`
`instR0Space` 📖	mathematical	—	`R0Space` `ContinuousMapZero` `instTopologicalSpace`	—	`Topology.IsInducing.r0Space` `ContinuousMap.instR0Space` `instContinuousMapClass` `Topology.IsEmbedding.toIsInducing` `isEmbedding_toContinuousMap`
`instR1Space` 📖	mathematical	—	`R1Space` `ContinuousMapZero` `instTopologicalSpace`	—	`Topology.IsInducing.r1Space` `ContinuousMap.instR1Space` `instContinuousMapClass` `Topology.IsEmbedding.toIsInducing` `isEmbedding_toContinuousMap`
`instRegularSpace` 📖	mathematical	—	`RegularSpace` `ContinuousMapZero` `instTopologicalSpace`	—	`Topology.IsInducing.regularSpace` `ContinuousMap.instRegularSpace` `instContinuousMapClass` `Topology.IsEmbedding.toIsInducing` `isEmbedding_toContinuousMap`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `ContinuousMapZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instSMul`	—	`ext` `SMulCommClass.smul_comm` `instContinuousMapClass`
`instSMulCommClass'` 📖	mathematical	—	`SMulCommClass` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instNonUnitalCommSemiring`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `ext` `SMulCommClass.smul_comm`
`instStarModule` 📖	mathematical	—	`StarModule` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instNonUnitalCommSemiring` `StarRing.toStarAddMonoid` `instStarRing` `instSMul`	—	`ext` `StarModule.star_smul`
`instT0Space` 📖	mathematical	—	`T0Space` `ContinuousMapZero` `instTopologicalSpace`	—	`Topology.IsEmbedding.t0Space` `ContinuousMap.instT0Space` `instContinuousMapClass` `isEmbedding_toContinuousMap`
`instT1Space` 📖	mathematical	—	`T1Space` `ContinuousMapZero` `instTopologicalSpace`	—	`Topology.IsEmbedding.t1Space` `ContinuousMap.instT1Space` `instContinuousMapClass` `isEmbedding_toContinuousMap`
`instT2Space` 📖	mathematical	—	`T2Space` `ContinuousMapZero` `instTopologicalSpace`	—	`Topology.IsEmbedding.t2Space` `ContinuousMap.instT2Space` `instContinuousMapClass` `isEmbedding_toContinuousMap`
`instT3Space` 📖	mathematical	—	`T3Space` `ContinuousMapZero` `instTopologicalSpace`	—	`Topology.IsEmbedding.t3Space` `ContinuousMap.instT3Space` `instContinuousMapClass` `isEmbedding_toContinuousMap`
`instTrivialStar` 📖	mathematical	—	`TrivialStar` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instNonUnitalCommSemiring` `StarRing.toStarAddMonoid` `instStarRing`	—	`DFunLike.ext` `TrivialStar.star_trivial`
`instZeroHomClass` 📖	mathematical	—	`ZeroHomClass` `ContinuousMapZero` `instFunLike`	—	`map_zero'`
`isClosedEmbedding_toContinuousMap` 📖	mathematical	—	`Topology.IsClosedEmbedding` `ContinuousMapZero` `ContinuousMap` `instTopologicalSpace` `ContinuousMap.compactOpen` `toContinuousMap` `instFunLike` `instContinuousMapClass`	—	`instContinuousMapClass` `isEmbedding_toContinuousMap` `range_toContinuousMap` `IsClosed.preimage` `ContinuousEvalConst.continuous_eval_const` `ContinuousMap.instContinuousEvalConst` `isClosed_singleton`
`isEmbedding_toContinuousMap` 📖	mathematical	—	`Topology.IsEmbedding` `ContinuousMapZero` `ContinuousMap` `instTopologicalSpace` `ContinuousMap.compactOpen` `toContinuousMap` `instFunLike` `instContinuousMapClass`	—	`instContinuousMapClass` `ext`
`isUniformEmbedding_comp` 📖	mathematical	`IsUniformEmbedding` `DFunLike.coe` `ContinuousMapZero` `UniformSpace.toTopologicalSpace` `instFunLike`	`IsUniformEmbedding` `ContinuousMapZero` `UniformSpace.toTopologicalSpace` `instUniformSpace` `comp`	—	`instContinuousMapClass` `IsUniformEmbedding.of_comp_iff` `isUniformEmbedding_toContinuousMap` `IsUniformEmbedding.comp` `ContinuousMap.isUniformEmbedding_comp`
`isUniformEmbedding_toContinuousMap` 📖	mathematical	—	`IsUniformEmbedding` `ContinuousMapZero` `UniformSpace.toTopologicalSpace` `ContinuousMap` `instUniformSpace` `ContinuousMap.compactConvergenceUniformSpace` `toContinuousMap` `instFunLike` `instContinuousMapClass`	—	`instContinuousMapClass` `ext`
`isometry_toContinuousMap` 📖	mathematical	—	`Isometry` `ContinuousMapZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMap` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `instMetricSpace` `ContinuousMap.instMetricSpace` `toContinuousMap`	—	—
`le_def` 📖	mathematical	—	`ContinuousMapZero` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `instFunLike`	—	—
`map_zero'` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toContinuousMap`	—	—
`mkD_apply_of_continuous` 📖	mathematical	`Continuous`	`DFunLike.coe` `ContinuousMapZero` `instFunLike` `mkD`	—	`mkD_of_continuous`
`mkD_apply_of_continuousOn` 📖	mathematical	`ContinuousOn` `Set` `Set.instMembership` `Set.Elem`	`DFunLike.coe` `ContinuousMapZero` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instFunLike` `mkD` `Set.restrict`	—	`ContinuousOn.restrict` `mkD_of_continuousOn` `Set.restrict_apply`
`mkD_eq_mkD_of_map_zero` 📖	mathematical	—	`toContinuousMap` `ContinuousMapZero` `instFunLike` `instContinuousMapClass` `mkD` `ContinuousMap.mkD`	—	`ContinuousMap.ext` `instContinuousMapClass` `toContinuousMap.congr_simp` `mkD_of_continuous` `ContinuousMap.mkD_of_continuous` `mkD_of_not_continuous` `ContinuousMap.mkD_of_not_continuous`
`mkD_eq_self` 📖	mathematical	—	`mkD` `DFunLike.coe` `ContinuousMapZero` `instFunLike`	—	`mkD_of_continuous` `ContinuousMap.continuous` `map_zero` `instZeroHomClass`
`mkD_of_continuous` 📖	mathematical	`Continuous`	`mkD`	—	—
`mkD_of_continuousOn` 📖	mathematical	`ContinuousOn` `Set` `Set.instMembership` `Set.Elem`	`mkD` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `ContinuousOn.restrict`	—	`mkD_of_continuous` `ContinuousOn.restrict`
`mkD_of_not_continuous` 📖	mathematical	`Continuous`	`mkD`	—	—
`mkD_of_not_continuousOn` 📖	mathematical	`ContinuousOn`	`mkD` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict`	—	`mkD_of_not_continuous` `continuousOn_iff_continuous_restrict`
`mkD_of_not_zero` 📖	mathematical	—	`mkD`	—	—
`nonUnitalStarAlgHom_postcomp_apply` 📖	mathematical	`Continuous` `DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `NonUnitalStarAlgHom.instFunLike`	`DFunLike.coe` `NonUnitalStarAlgHom` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instNonUnitalCommSemiring` `Module.toDistribMulAction` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `instModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `instStarRing` `NonUnitalStarAlgHom.instFunLike` `nonUnitalStarAlgHom_postcomp` `comp`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring`
`nonUnitalStarAlgHom_precomp_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instNonUnitalCommSemiring` `Module.toDistribMulAction` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `instStarRing` `NonUnitalStarAlgHom.instFunLike` `nonUnitalStarAlgHom_precomp` `comp`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`norm_def` 📖	mathematical	—	`Norm.norm` `ContinuousMapZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNorm` `ContinuousMap` `ContinuousMap.instNorm` `toContinuousMap` `instFunLike` `instContinuousMapClass`	—	—
`postcomp_injective` 📖	mathematical	`DFunLike.coe` `ContinuousMapZero` `instFunLike`	`ContinuousMapZero` `comp`	—	`ext`
`range_toContinuousMap` 📖	mathematical	—	`Set.range` `ContinuousMap` `ContinuousMapZero` `toContinuousMap` `instFunLike` `instContinuousMapClass` `setOf` `DFunLike.coe` `ContinuousMap.instFunLike`	—	`Set.ext` `instContinuousMapClass` `map_zero` `instZeroHomClass`
`toContinuousMapCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommSemiring.toSemiring` `instTopologicalSpace` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `ContinuousMap` `ContinuousMap.compactOpen` `ContinuousMap.instAddCommMonoidOfContinuousAdd` `instModule` `ContinuousMap.module` `ContinuousLinearMap.funLike` `toContinuousMapCLM` `toContinuousMap` `instFunLike`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring`
`toContinuousMapHom_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `ContinuousMapZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ContinuousMap` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instNonUnitalCommSemiring` `Module.toDistribMulAction` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `instStarRing` `ContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring` `ContinuousMap.instDistribMulActionOfContinuousConstSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `ContinuousMap.instStar` `NonUnitalStarAlgHom.instFunLike` `toContinuousMapHom` `toContinuousMap` `instFunLike`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`toContinuousMap_id` 📖	mathematical	—	`toContinuousMap` `ContinuousMapZero` `Set.Elem` `Set.zeroOfFactMem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instFunLike` `instContinuousMapClass` `id` `ContinuousMap.restrict` `ContinuousMap.id`	—	`instContinuousMapClass`
`toContinuousMap_injective` 📖	mathematical	—	`ContinuousMapZero` `ContinuousMap` `toContinuousMap` `instFunLike` `instContinuousMapClass`	—	`instContinuousMapClass` `map_zero'`

Set

Definitions

Name	Category	Theorems
`zeroOfFactMem` 📖	CompOp	10 math math: `continuous_cfcₙHomSuperset_left`, `ContinuousMapZero.toContinuousMap_id`, `ContinuousMapZero.id_toFun`, `ContinuousMapZero.mul_nonUnitalStarAlgHom_apply_eq_zero`, `cfcₙHomSuperset_id`, `cfcₙHomSuperset_continuous`, `ContinuousMapZero.elemental_eq_top`, `ContinuousMapZero.adjoin_id_dense`, `cfcₙHomSuperset_apply`, `ContinuousMapZero.nonUnitalStarAlgHom_apply_mul_eq_zero`

UniformEquiv

Definitions

Name	Category	Theorems
`arrowCongrLeft₀` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`ContinuousMapZero` 📖	CompData	137 math math: `ContinuousMapZero.coe_star`, `ContinuousMapZero.postcomp_injective`, `cfcₙ_def`, `continuous_cfcₙHomSuperset_left`, `cfcₙL_integral`, `norm_cfcₙHom`, `ContinuousMapZero.instContinuousEval`, `cfcₙHom_mono`, `NonUnitalIsometricContinuousFunctionalCalculus.isometric`, `cfcₙHom_apply_mem_elemental`, `ContinuousMapZero.isEmbedding_toContinuousMap`, `ContinuousMapZero.instSMulCommClass`, `cfcₙHom_of_cfcHom_injective`, `ContinuousMapZero.instIsScalarTower`, `ContinuousMapZero.toContinuousMap_id`, `isClosedEmbedding_cfcₙAux`, `ContinuousMapZero.id_toFun`, `ContinuousMapZero.instCanLift`, `ContinuousMapZero.aeStronglyMeasurable_mkD_of_uncurry`, `QuasispectrumRestricts.nonUnitalStarAlgHom_id`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal`, `ContinuousMapZero.coe_mul`, `cfcₙHom_mem_elemental`, `ContinuousMapZero.isometry_toContinuousMap`, `cfcₙ_eq_cfcₙL_mkD`, `ContinuousMapZero.coe_add`, `ContinuousMapZero.ext_iff`, `cfcₙ_apply_mkD`, `cfcₙHom_id`, `inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux`, `range_cfcₙHom`, `ContinuousMapZero.hasFiniteIntegral_of_bound`, `ContinuousMapZero.instCompleteSpaceOfT1SpaceOfContinuousMap`, `NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding`, `ContinuousMapZero.instStarOrderedRing`, `cfcₙHom_integral`, `ContinuousMapZero.integral_apply`, `cfcₙAux_id`, `isometry_cfcₙHom`, `cfcₙHom_predicate`, `ContinuousMapZero.instT0Space`, `cfcₙHom_comp`, `ContinuousMapZero.coe_mk`, `Commute.cfcₙHom`, `QuasispectrumRestricts.continuous_nonUnitalStarAlgHom`, `ContinuousMapZero.toContinuousMapCLM_apply`, `range_cfcₙ_eq_range_cfcₙHom`, `range_cfcₙHom_le`, `ContinuousMapZero.instT1Space`, `ContinuousMapZero.coe_neg`, `ContinuousMapZero.nonUnitalStarAlgHom_precomp_apply`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `ContinuousMapZero.coe_smul`, `ContinuousMapZero.continuous_comp_left`, `cfcₙHom_isClosedEmbedding`, `ContinuousMapZero.instContinuousEvalConst`, `cfcₙHom_le_iff`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply`, `ContinuousMapZero.continuous_postcomp`, `ContinuousMapZero.norm_def`, `ContinuousMapZero.mul_nonUnitalStarAlgHom_apply_eq_zero`, `ContinuousMapZero.instR0Space`, `cfcₙHom_eq_cfcₙ_extend`, `cfcₙAux_injective`, `QuasispectrumRestricts.nonUnitalStarAlgHom_injective`, `ContinuousMapZero.instTrivialStar`, `ContinuousMapZero.mkD_eq_self`, `ContinuousMapZero.toNNReal_mul_add_neg_mul_add_mul_neg_eq`, `ContinuousMapZero.toContinuousMapHom_toNNReal`, `cfcₙHom_map_quasispectrum`, `QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom`, `ContinuousMapZero.instContinuousNeg`, `spec_cfcₙAux`, `cfcₙHom_injective`, `cfcₙHomSuperset_id`, `ContinuousMapZero.evalCLM_apply`, `ContinuousMapZero.toNNReal_add_add_neg_add_neg_eq`, `ContinuousMapZero.isUniformEmbedding_comp`, `ContinuousMapZero.instSMulCommClass'`, `ContinuousMapZero.instContinuousMapClass`, `nnnorm_cfcₙHom`, `ContinuousMapZero.le_def`, `continuous_cfcₙHom_of_cfcHom`, `isClosedEmbedding_cfcₙHom_of_cfcHom`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective`, `IsSelfAdjoint.commute_cfcₙHom`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `ContinuousMapZero.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry`, `NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate`, `ContinuousMapZero.instT2Space`, `ContinuousMapZero.coe_sum`, `ContinuousMapZero.toContinuousMapHom_apply`, `cfcₙAux_mem_range_inr`, `ContinuousMapZero.hasFiniteIntegral_mkD_restrict_of_bound`, `ContinuousMapZero.coe_sub`, `ContinuousMapZero.instCStarRing`, `cfcₙHom_continuous`, `cfcₙHomSuperset_continuous`, `ContinuousMapZero.isUniformEmbedding_toContinuousMap`, `cfcₙ_apply_pi`, `ContinuousMapZero.mkD_apply_of_continuous`, `ContinuousMapZero.mkD_eq_mkD_of_map_zero`, `ContinuousMapZero.aeStronglyMeasurable_mkD_restrict_of_uncurry`, `ContinuousMapZero.instRegularSpace`, `ContinuousMapZero.continuous_precomp`, `continuous_cfcₙAux`, `ContinuousMapZero.comp_apply`, `cfcₙ_eq_cfcₙL`, `cfcₙL_apply`, `ContinuousMapZero.toNNReal_neg_smul`, `ContinuousMapZero.nonUnitalStarAlgHom_postcomp_apply`, `ContinuousMapZero.aeStronglyMeasurable_restrict_mkD_of_uncurry`, `ContinuousMapZero.elemental_eq_top`, `ContinuousMapZero.adjoin_id_dense`, `ContinuousMapZero.toNNReal_smul`, `ContinuousMapZero.instIsScalarTower'`, `ContinuousMapZero.instR1Space`, `ContinuousMapZero.mkD_apply_of_continuousOn`, `ContinuousMapZero.hasFiniteIntegral_mkD_of_bound`, `ContinuousMapZero.instT3Space`, `cfcₙL_integrable`, `ContinuousMapZero.toContinuousMap_injective`, `cfcₙHom_of_cfcHom_map_quasispectrum`, `ContinuousMapZero.instStarModule`, `cfcₙHomSuperset_apply`, `cfcₙ_apply`, `ContinuousMapZero.continuous_toNNReal`, `ContinuousMapZero.coe_toContinuousMapHom`, `cfcₙHom_nonneg_iff`, `ContinuousMapZero.instZeroHomClass`, `ContinuousMapZero.toNNReal_apply`, `ContinuousMapZero.nonUnitalStarAlgHom_apply_mul_eq_zero`, `ContinuousMapZero.coeFnAddMonoidHom_apply`, `NonUnitalStarAlgHom.continuous_realContinuousMapZeroOfNNReal`, `ContinuousMapZero.isClosedEmbedding_toContinuousMap`, `ContinuousMapZero.range_toContinuousMap`, `ContinuousMapZero.coe_zero`

---

← Back to Index