Compact

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

Statistics

Metric	Count
Definitions addEquivBoundedOfCompact, equivBoundedOfCompact, instMetricSpace, instNonUnitalNormedCommRing, instNonUnitalNormedRing, instNonUnitalSeminormedCommRing, instNonUnitalSeminormedRing, instNorm, instNormedAddCommGroup, instNormedAlgebra, instNormedCommRing, instNormedRing, instPseudoMetricSpace, instSeminormedAddCommGroup, instSeminormedCommRing, instSeminormedRing, isometryEquivBoundedOfCompact, linearIsometryBoundedOfCompact, modulus, normedSpace	20
Theorems dist_mkOfCompact, dist_toContinuousMap, mkOfCompact_star, norm_mkOfCompact, norm_toContinuousMap_eq, addEquivBoundedOfCompact_apply, addEquivBoundedOfCompact_symm_apply, apply_le_norm, dist_apply_le_dist, dist_eq_iSup, dist_le, dist_le_iff_of_nonempty, dist_le_two_norm, dist_lt_iff, dist_lt_iff_of_nonempty, dist_lt_of_dist_lt_modulus, dist_lt_of_nonempty, edist_eq_iSup, enorm_eq_iSup_enorm, equivBoundedOfCompact_apply, equivBoundedOfCompact_symm_apply, instCStarRing, instCompactSpaceElemCoeCompacts, instIsBoundedSMul, instNormOneClassOfNonempty, instNormedStarGroup, isUniformEmbedding_equivBoundedOfCompact, isUniformInducing_equivBoundedOfCompact, isometryEquivBoundedOfCompact_apply, isometryEquivBoundedOfCompact_symm_apply, isometryEquivBoundedOfCompact_toEquiv, linearIsometryBoundedOfCompact_apply_apply, linearIsometryBoundedOfCompact_of_compact_toEquiv, linearIsometryBoundedOfCompact_symm_apply, linearIsometryBoundedOfCompact_toAddEquiv, linearIsometryBoundedOfCompact_toIsometryEquiv, modulus_pos, neg_norm_le_apply, nndist_eq_iSup, nnnorm_eq_iSup_nnnorm, nnnorm_lt_iff, nnnorm_lt_iff_of_nonempty, nnnorm_smul_const, norm_coe_le_norm, norm_eq_iSup_norm, norm_le, norm_le_of_nonempty, norm_lt_iff, norm_lt_iff_of_nonempty, norm_restrict_mono_set, norm_smul_const, summable_of_locally_summable_norm, uniform_continuity	53
Total	73

BoundedContinuousFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_mkOfCompact 📖	mathematical	—	Dist.dist BoundedContinuousFunction instDist mkOfCompact ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toDist ContinuousMap.instPseudoMetricSpace	—	—
dist_toContinuousMap 📖	mathematical	—	Dist.dist ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toDist ContinuousMap.instPseudoMetricSpace toContinuousMap BoundedContinuousFunction instDist	—	—
mkOfCompact_star 📖	mathematical	—	mkOfCompact SeminormedAddCommGroup.toPseudoMetricSpace Star.star ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedStarGroup.to_continuousStar BoundedContinuousFunction instAddMonoid instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup instStarAddMonoid	—	NormedStarGroup.to_continuousStar
norm_mkOfCompact 📖	mathematical	—	Norm.norm BoundedContinuousFunction SeminormedAddCommGroup.toPseudoMetricSpace instNorm mkOfCompact ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ContinuousMap.instNorm	—	—
norm_toContinuousMap_eq 📖	mathematical	—	Norm.norm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMap.instNorm toContinuousMap BoundedContinuousFunction instNorm	—	—

ContinuousMap

Definitions

Name	Category	Theorems
addEquivBoundedOfCompact 📖	CompOp	3 math math: addEquivBoundedOfCompact_apply, linearIsometryBoundedOfCompact_toAddEquiv, addEquivBoundedOfCompact_symm_apply
equivBoundedOfCompact 📖	CompOp	6 math math: isUniformInducing_equivBoundedOfCompact, linearIsometryBoundedOfCompact_of_compact_toEquiv, equivBoundedOfCompact_apply, isometryEquivBoundedOfCompact_toEquiv, equivBoundedOfCompact_symm_apply, isUniformEmbedding_equivBoundedOfCompact
instMetricSpace 📖	CompOp	4 math math: ContinuousMapZero.isometry_toContinuousMap, gelfandTransform_isometry, IsometricContinuousFunctionalCalculus.isometric, isometry_cfcHom
instNonUnitalNormedCommRing 📖	CompOp	—
instNonUnitalNormedRing 📖	CompOp	1 math math: instCStarRing
instNonUnitalSeminormedCommRing 📖	CompOp	—
instNonUnitalSeminormedRing 📖	CompOp	8 math math: abs_mem_subalgebra_closure, continuousMap_mem_subalgebra_closure_of_separatesPoints, NormedSpace.exp_continuousMap_eq, sup_mem_subalgebra_closure, inf_mem_subalgebra_closure, subalgebra_topologicalClosure_eq_top_of_separatesPoints, comp_attachBound_mem_closure, starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
instNorm 📖	CompOp	27 math math: attachBound_apply_coe, dist_le_two_norm, norm_le, PadicInt.norm_mahlerTerm, norm_coe_le_norm, fourier_norm, norm_le_of_nonempty, isBigO_norm_Icc_restrict_atTop, norm_eq_iSup_norm, BoundedContinuousFunction.norm_toContinuousMap_eq, IsUltrametricDist.norm_fwdDiff_iter_apply_le, exists_mem_subalgebra_near_continuousMap_of_separatesPoints, UnitAddTorus.mFourier_norm, exists_polynomial_near_continuousMap, ContinuousMapZero.norm_def, norm_lt_iff, norm_lt_iff_of_nonempty, neg_norm_le_apply, norm_restrict_mono_set, apply_le_norm, BoundedContinuousFunction.norm_mkOfCompact, isBigO_norm_Icc_restrict_atBot, PadicInt.norm_mahler_eq, norm_cfcHom, norm_smul_const, isBigO_norm_restrict_cocompact, instNormOneClassOfNonempty
instNormedAddCommGroup 📖	CompOp	3 math math: integral_apply, cfcHom_integral, cfcL_integral
instNormedAlgebra 📖	CompOp	1 math math: WeakDual.CharacterSpace.homeoEval_naturality
instNormedCommRing 📖	CompOp	—
instNormedRing 📖	CompOp	4 math math: WeakDual.CharacterSpace.homeoEval_naturality, comp_attachBound_mem_closure, polynomial_comp_attachBound, polynomial_comp_attachBound_mem
instPseudoMetricSpace 📖	CompOp	20 math math: dist_lt_iff, isUltrametricDist, dist_le, dist_lt_of_nonempty, BoundedContinuousFunction.dist_toContinuousMap, dist_apply_le_dist, UniformFun.isometry_ofFun_continuousMap, dist_lt_iff_of_nonempty, instIsBoundedSMul, nndist_eq_iSup, isometryEquivBoundedOfCompact_toEquiv, UniformOnFun.edist_continuousRestrict, isometryEquivBoundedOfCompact_symm_apply, UniformOnFun.edist_continuousRestrict_of_singleton, UniformFun.edist_continuousMapMk, isometryEquivBoundedOfCompact_apply, BoundedContinuousFunction.dist_mkOfCompact, dist_le_iff_of_nonempty, edist_eq_iSup, dist_eq_iSup
instSeminormedAddCommGroup 📖	CompOp	25 math math: UnitAddTorus.mFourierSubalgebra_closure_eq_top, polynomialFunctions.starClosure_topologicalClosure, toLp_norm_le, instNormedStarGroup, hasFiniteIntegral_of_bound, linearIsometryBoundedOfCompact_symm_apply, linearIsometryBoundedOfCompact_of_compact_toEquiv, toLp_def, nnnorm_lt_iff, nnnorm_smul_const, toLp_norm_eq_toLp_norm_coe, nnnorm_lt_iff_of_nonempty, linearIsometryBoundedOfCompact_toAddEquiv, nnnorm_eq_iSup_nnnorm, linearIsometryBoundedOfCompact_apply_apply, hasFiniteIntegral_mkD_of_bound, PadicInt.mahlerEquiv_apply, hasFiniteIntegral_mkD_restrict_of_bound, fourierSubalgebra_closure_eq_top, elemental_id_eq_top, nnnorm_cfcHom, PadicInt.mahlerEquiv_symm_apply, starSubalgebra_topologicalClosure_eq_top_of_separatesPoints, enorm_eq_iSup_enorm, linearIsometryBoundedOfCompact_toIsometryEquiv
instSeminormedCommRing 📖	CompOp	—
instSeminormedRing 📖	CompOp	—
isometryEquivBoundedOfCompact 📖	CompOp	4 math math: isometryEquivBoundedOfCompact_toEquiv, isometryEquivBoundedOfCompact_symm_apply, isometryEquivBoundedOfCompact_apply, linearIsometryBoundedOfCompact_toIsometryEquiv
linearIsometryBoundedOfCompact 📖	CompOp	6 math math: linearIsometryBoundedOfCompact_symm_apply, linearIsometryBoundedOfCompact_of_compact_toEquiv, toLp_def, linearIsometryBoundedOfCompact_toAddEquiv, linearIsometryBoundedOfCompact_apply_apply, linearIsometryBoundedOfCompact_toIsometryEquiv
modulus 📖	CompOp	1 math math: modulus_pos
normedSpace 📖	CompOp	5 math math: integral_apply, toLp_norm_le, cfcHom_integral, toLp_norm_eq_toLp_norm_coe, cfcL_integral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addEquivBoundedOfCompact_apply 📖	mathematical	—	DFunLike.coe AddEquiv ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace BoundedContinuousFunction instAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup LipschitzAdd.continuousAdd BoundedContinuousFunction.instAdd instBoundedAddOfLipschitzAdd EquivLike.toFunLike AddEquiv.instEquivLike addEquivBoundedOfCompact BoundedContinuousFunction.mkOfCompact	—	LipschitzAdd.continuousAdd instBoundedAddOfLipschitzAdd
addEquivBoundedOfCompact_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv BoundedContinuousFunction ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace BoundedContinuousFunction.instAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup instBoundedAddOfLipschitzAdd LipschitzAdd.continuousAdd instAdd EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm addEquivBoundedOfCompact AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass BoundedContinuousFunction.instAddMonoid instAddZeroClassOfContinuousAdd AddMonoidHom.instFunLike BoundedContinuousFunction.toContinuousMapAddMonoidHom	—	instBoundedAddOfLipschitzAdd LipschitzAdd.continuousAdd
apply_le_norm 📖	mathematical	—	Real Real.instLE DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instFunLike Norm.norm instNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	—	le_trans le_abs le_refl norm_coe_le_norm
dist_apply_le_dist 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instFunLike instPseudoMetricSpace	—	—
dist_eq_iSup 📖	mathematical	—	Dist.dist ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toDist instPseudoMetricSpace iSup Real Real.instSupSet DFunLike.coe instFunLike	—	IsometryEquiv.dist_eq BoundedContinuousFunction.dist_eq_iSup
dist_le 📖	mathematical	Real Real.instLE Real.instZero	Dist.dist ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toDist instPseudoMetricSpace DFunLike.coe instFunLike	—	BoundedContinuousFunction.dist_le
dist_le_iff_of_nonempty 📖	mathematical	—	Real Real.instLE Dist.dist ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toDist instPseudoMetricSpace DFunLike.coe instFunLike	—	—
dist_le_two_norm 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instFunLike Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Norm.norm instNorm	—	BoundedContinuousFunction.dist_le_two_norm
dist_lt_iff 📖	mathematical	Real Real.instLT Real.instZero	Dist.dist ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toDist instPseudoMetricSpace DFunLike.coe instFunLike	—	BoundedContinuousFunction.dist_mkOfCompact BoundedContinuousFunction.dist_lt_iff_of_compact
dist_lt_iff_of_nonempty 📖	mathematical	—	Real Real.instLT Dist.dist ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toDist instPseudoMetricSpace DFunLike.coe instFunLike	—	—
dist_lt_of_dist_lt_modulus 📖	mathematical	Real Real.instLT Real.instZero Dist.dist PseudoMetricSpace.toDist modulus	DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instFunLike	—	uniform_continuity
dist_lt_of_nonempty 📖	mathematical	Real Real.instLT Dist.dist PseudoMetricSpace.toDist DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instFunLike	instPseudoMetricSpace	—	dist_lt_iff_of_nonempty
edist_eq_iSup 📖	mathematical	—	EDist.edist ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace instPseudoMetricSpace iSup ENNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder DFunLike.coe instFunLike	—	IsometryEquiv.edist_eq BoundedContinuousFunction.edist_eq_iSup
enorm_eq_iSup_enorm 📖	mathematical	—	ENorm.enorm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup instSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm iSup ENNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder DFunLike.coe instFunLike	—	BoundedContinuousFunction.enorm_eq_iSup_enorm
equivBoundedOfCompact_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace BoundedContinuousFunction EquivLike.toFunLike Equiv.instEquivLike equivBoundedOfCompact BoundedContinuousFunction.mkOfCompact	—	—
equivBoundedOfCompact_symm_apply 📖	mathematical	—	DFunLike.coe Equiv BoundedContinuousFunction ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivBoundedOfCompact BoundedContinuousFunction.toContinuousMap	—	—
instCStarRing 📖	mathematical	—	CStarRing ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing instNonUnitalNormedRing instStarRingOfContinuousStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup StarRing.toStarAddMonoid CStarRing.to_normedStarGroup	—	IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup sq Real.le_sqrt norm_nonneg norm_le Real.sqrt_nonneg CStarRing.norm_star_mul_self norm_coe_le_norm IsTopologicalSemiring.toContinuousMul
instCompactSpaceElemCoeCompacts 📖	mathematical	—	CompactSpace Set.Elem SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike instTopologicalSpaceSubtype Set Set.instMembership	—	TopologicalSpace.Compacts.instCompactSpaceSubtypeMem
instIsBoundedSMul 📖	mathematical	—	IsBoundedSMul ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpace instZero instSMul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul dist_smul_pair BoundedContinuousFunction.instIsBoundedSMul dist_pair_smul
instNormOneClassOfNonempty 📖	mathematical	—	NormOneClass ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instNorm instOne	—	NormOneClass.norm_one BoundedContinuousFunction.instNormOneClass
instNormedStarGroup 📖	mathematical	—	NormedStarGroup ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instSeminormedAddCommGroup starAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NormedStarGroup.to_continuousStar	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedStarGroup.to_continuousStar BoundedContinuousFunction.norm_mkOfCompact instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd BoundedContinuousFunction.mkOfCompact_star norm_star BoundedContinuousFunction.instNormedStarGroup le_refl
isUniformEmbedding_equivBoundedOfCompact 📖	mathematical	—	IsUniformEmbedding ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace BoundedContinuousFunction compactConvergenceUniformSpace BoundedContinuousFunction.instPseudoMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivBoundedOfCompact	—	isUniformInducing_equivBoundedOfCompact Equiv.injective
isUniformInducing_equivBoundedOfCompact 📖	mathematical	—	IsUniformInducing ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace BoundedContinuousFunction compactConvergenceUniformSpace BoundedContinuousFunction.instPseudoMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivBoundedOfCompact	—	IsUniformInducing.mk' Filter.HasBasis.mem_iff hasBasis_compactConvergenceUniformity Metric.uniformity_basis_dist_le BoundedContinuousFunction.dist_le LT.lt.le isCompact_univ Set.mem_univ
isometryEquivBoundedOfCompact_apply 📖	mathematical	—	DFunLike.coe IsometryEquiv ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace BoundedContinuousFunction PseudoMetricSpace.toPseudoEMetricSpace instPseudoMetricSpace BoundedContinuousFunction.instPseudoMetricSpace EquivLike.toFunLike IsometryEquiv.instEquivLike isometryEquivBoundedOfCompact BoundedContinuousFunction.mkOfCompact	—	—
isometryEquivBoundedOfCompact_symm_apply 📖	mathematical	—	DFunLike.coe IsometryEquiv BoundedContinuousFunction ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace BoundedContinuousFunction.instPseudoMetricSpace instPseudoMetricSpace EquivLike.toFunLike IsometryEquiv.instEquivLike IsometryEquiv.symm isometryEquivBoundedOfCompact BoundedContinuousFunction.toContinuousMap	—	—
isometryEquivBoundedOfCompact_toEquiv 📖	mathematical	—	IsometryEquiv.toEquiv ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace BoundedContinuousFunction PseudoMetricSpace.toPseudoEMetricSpace instPseudoMetricSpace BoundedContinuousFunction.instPseudoMetricSpace isometryEquivBoundedOfCompact equivBoundedOfCompact	—	—
linearIsometryBoundedOfCompact_apply_apply 📖	mathematical	—	DFunLike.coe BoundedContinuousFunction SeminormedAddCommGroup.toPseudoMetricSpace BoundedContinuousFunction.instFunLike LinearIsometryEquiv Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instSeminormedAddCommGroup BoundedContinuousFunction.instSeminormedAddCommGroup module AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup 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 SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid BoundedContinuousFunction.instModule EquivLike.toFunLike LinearIsometryEquiv.instEquivLike linearIsometryBoundedOfCompact instFunLike	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul
linearIsometryBoundedOfCompact_of_compact_toEquiv 📖	mathematical	—	LinearEquiv.toEquiv ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace BoundedContinuousFunction Ring.toSemiring NormedRing.toRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instSeminormedAddCommGroup BoundedContinuousFunction.instSeminormedAddCommGroup module SeminormedAddCommGroup.toIsTopologicalAddGroup 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 SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid BoundedContinuousFunction.instModule RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearIsometryEquiv.toLinearEquiv linearIsometryBoundedOfCompact equivBoundedOfCompact	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul RingHomInvPair.ids
linearIsometryBoundedOfCompact_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids BoundedContinuousFunction SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace BoundedContinuousFunction.instSeminormedAddCommGroup instSeminormedAddCommGroup BoundedContinuousFunction.instModule SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup module SeminormedAddCommGroup.toIsTopologicalAddGroup 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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm linearIsometryBoundedOfCompact BoundedContinuousFunction.toContinuousMap	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul
linearIsometryBoundedOfCompact_toAddEquiv 📖	mathematical	—	AddEquivClass.toAddEquiv LinearEquiv Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace BoundedContinuousFunction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instSeminormedAddCommGroup BoundedContinuousFunction.instSeminormedAddCommGroup module SeminormedAddCommGroup.toIsTopologicalAddGroup 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 SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid BoundedContinuousFunction.instModule DFinsupp.instEquivLikeLinearEquiv instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup BoundedContinuousFunction.instAdd instBoundedAddOfLipschitzAdd SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddCommGroup.to_lipschitzAdd SemilinearEquivClass.toAddEquivClass instAddCommMonoidOfContinuousAdd BoundedContinuousFunction.instAddCommMonoid LinearEquiv.instSemilinearEquivClass LinearIsometryEquiv.toLinearEquiv linearIsometryBoundedOfCompact addEquivBoundedOfCompact	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd RingHomInvPair.ids UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass
linearIsometryBoundedOfCompact_toIsometryEquiv 📖	mathematical	—	LinearIsometryEquiv.toIsometryEquiv ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace BoundedContinuousFunction Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instSeminormedAddCommGroup BoundedContinuousFunction.instSeminormedAddCommGroup module AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup 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 SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid BoundedContinuousFunction.instModule linearIsometryBoundedOfCompact isometryEquivBoundedOfCompact	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul
modulus_pos 📖	mathematical	Real Real.instLT Real.instZero	modulus	—	uniform_continuity
neg_norm_le_apply 📖	mathematical	—	Real Real.instLE Real.instNeg Norm.norm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing DFunLike.coe instFunLike	—	le_trans neg_le_neg Real.instIsOrderedAddMonoid norm_coe_le_norm neg_le IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add neg_le_abs
nndist_eq_iSup 📖	mathematical	—	NNDist.nndist ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toNNDist instPseudoMetricSpace iSup NNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder NNReal.instConditionallyCompleteLinearOrderBot DFunLike.coe instFunLike	—	IsometryEquiv.nndist_eq BoundedContinuousFunction.nndist_eq_iSup
nnnorm_eq_iSup_nnnorm 📖	mathematical	—	NNNorm.nnnorm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup instSeminormedAddCommGroup iSup NNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder NNReal.instConditionallyCompleteLinearOrderBot DFunLike.coe instFunLike	—	BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm
nnnorm_lt_iff 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal	NNNorm.nnnorm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup instSeminormedAddCommGroup DFunLike.coe instFunLike	—	norm_lt_iff
nnnorm_lt_iff_of_nonempty 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup instSeminormedAddCommGroup DFunLike.coe instFunLike	—	norm_lt_iff_of_nonempty
nnnorm_smul_const 📖	mathematical	—	NNNorm.nnnorm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup instSeminormedAddCommGroup SeminormedRing.toPseudoMetricSpace instSMul' Ring.toSemiring SeminormedRing.toRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormSMulClass.toIsBoundedSMul const NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing	—	IsBoundedSMul.continuousSMul NormSMulClass.toIsBoundedSMul nnnorm_eq_iSup_nnnorm nnnorm_smul NNReal.iSup_mul
norm_coe_le_norm 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instFunLike instNorm	—	BoundedContinuousFunction.norm_coe_le_norm
norm_eq_iSup_norm 📖	mathematical	—	Norm.norm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instNorm iSup Real Real.instSupSet SeminormedAddCommGroup.toNorm DFunLike.coe instFunLike	—	BoundedContinuousFunction.norm_eq_iSup_norm
norm_le 📖	mathematical	Real Real.instLE Real.instZero	Norm.norm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instNorm SeminormedAddCommGroup.toNorm DFunLike.coe instFunLike	—	BoundedContinuousFunction.norm_le
norm_le_of_nonempty 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instNorm SeminormedAddCommGroup.toNorm DFunLike.coe instFunLike	—	BoundedContinuousFunction.norm_le_of_nonempty
norm_lt_iff 📖	mathematical	Real Real.instLT Real.instZero	Norm.norm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instNorm SeminormedAddCommGroup.toNorm DFunLike.coe instFunLike	—	BoundedContinuousFunction.norm_lt_iff_of_compact
norm_lt_iff_of_nonempty 📖	mathematical	—	Real Real.instLT Norm.norm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instNorm SeminormedAddCommGroup.toNorm DFunLike.coe instFunLike	—	BoundedContinuousFunction.norm_lt_iff_of_nonempty_compact
norm_restrict_mono_set 📖	mathematical	TopologicalSpace.Compacts Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Compacts.instPartialOrder	Real Real.instLE Norm.norm ContinuousMap Set.Elem SetLike.coe TopologicalSpace.Compacts.instSetLike instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instNorm instCompactSpaceElemCoeCompacts restrict	—	instCompactSpaceElemCoeCompacts norm_le norm_nonneg norm_coe_le_norm
norm_smul_const 📖	mathematical	—	Norm.norm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instNorm SeminormedRing.toPseudoMetricSpace instSMul' Ring.toSemiring SeminormedRing.toRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormSMulClass.toIsBoundedSMul const Real Real.instMul NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing SeminormedAddCommGroup.toNorm	—	IsBoundedSMul.continuousSMul NormSMulClass.toIsBoundedSMul nnnorm_smul_const
summable_of_locally_summable_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm ContinuousMap Set.Elem SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike instTopologicalSpaceSubtype Set Set.instMembership SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNorm instCompactSpaceElemCoeCompacts restrict SummationFilter.unconditional	instAddCommMonoidOfContinuousAdd ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup compactOpen	—	instCompactSpaceElemCoeCompacts IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup exists_tendsto_compactOpen_iff_forall instWeaklyLocallyCompactSpaceOfLocallyCompactSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotFinsetFilterOfNeBot SummationFilter.instNeBotUnconditional CanLift.prf TopologicalSpace.Compacts.instCanLiftSetCoeIsCompact ext coe_sum Finset.sum_apply Finset.sum_congr Summable.of_norm instCompleteSpaceOfCompactlyCoherentSpace CompactlyCoherentSpace.of_weaklyLocallyCompactSpace instWeaklyLocallyCompactSpaceOfCompactSpace
uniform_continuity 📖	mathematical	Real Real.instLT Real.instZero	Dist.dist PseudoMetricSpace.toDist DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instFunLike	—	Metric.uniformContinuous_iff CompactSpace.uniformContinuous_of_continuous continuous

---

← Back to Index