BoundedCompactlySupported

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

Statistics

Metric	Count
Definitions «termC_cb(_,_)»»), compactlySupported, instSMulContinuousMapSubtypeBoundedContinuousFunctionMemTwoSidedIdealCompactlySupported, ofCompactSupport	4
Theorems compactlySupported_eq_top, compactlySupported_eq_top_iff, compactlySupported_eq_top_of_isCompact, exist_norm_eq, mem_compactlySupported, norm_lt_iff_of_compactlySupported, norm_lt_iff_of_nonempty_compactlySupported, ofCompactSupport_mem	8
Total	12

BoundedContinuousFunction

Definitions

Name	Category	Theorems
«termC_cb(_,_)» 📖» "API Documentation")	CompOp	—

(root)

Definitions

Name	Category	Theorems
compactlySupported 📖	CompOp	5 math math: compactlySupported_eq_top_of_isCompact, compactlySupported_eq_top, compactlySupported_eq_top_iff, mem_compactlySupported, ofCompactSupport_mem
instSMulContinuousMapSubtypeBoundedContinuousFunctionMemTwoSidedIdealCompactlySupported 📖	CompOp	—
ofCompactSupport 📖	CompOp	1 math math: ofCompactSupport_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactlySupported_eq_top 📖	mathematical	—	compactlySupported Top.top TwoSidedIdeal BoundedContinuousFunction NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalRing.toNonUnitalNonAssocRing BoundedContinuousFunction.instNonUnitalRing TwoSidedIdeal.instTop	—	compactlySupported_eq_top_of_isCompact CompactSpace.isCompact_univ
compactlySupported_eq_top_iff 📖	mathematical	—	compactlySupported Top.top TwoSidedIdeal BoundedContinuousFunction NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalRing.toNonUnitalNonAssocRing BoundedContinuousFunction.instNonUnitalRing TwoSidedIdeal.instTop IsCompact Set.univ	—	exists_ne Function.support_const IsClosed.closure_eq HasCompactSupport.isCompact mem_compactlySupported compactlySupported_eq_top_of_isCompact
compactlySupported_eq_top_of_isCompact 📖	mathematical	IsCompact Set.univ	compactlySupported Top.top TwoSidedIdeal BoundedContinuousFunction NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalRing.toNonUnitalNonAssocRing BoundedContinuousFunction.instNonUnitalRing TwoSidedIdeal.instTop	—	eq_top_iff IsCompact.of_isClosed_subset isClosed_tsupport Set.subset_univ
exist_norm_eq 📖	mathematical	BoundedContinuousFunction NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing TwoSidedIdeal NonUnitalRing.toNonUnitalNonAssocRing BoundedContinuousFunction.instNonUnitalRing SetLike.instMembership TwoSidedIdeal.setLike compactlySupported	Norm.norm NonUnitalNormedRing.toNorm DFunLike.coe BoundedContinuousFunction.instFunLike BoundedContinuousFunction.instNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup	—	IsCompact.exists_isMaxOn instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid mem_compactlySupported Continuous.continuousOn Continuous.norm ContinuousMapClass.map_continuous BoundedContinuousMapClass.toContinuousMapClass BoundedContinuousFunction.instBoundedContinuousMapClass le_antisymm BoundedContinuousFunction.norm_coe_le_norm BoundedContinuousFunction.norm_le norm_nonneg image_eq_zero_of_notMem_tsupport norm_zero DFunLike.ext'_iff BoundedContinuousFunction.coe_zero tsupport_eq_empty_iff Set.not_nonempty_iff_eq_empty
mem_compactlySupported 📖	mathematical	—	BoundedContinuousFunction NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing TwoSidedIdeal NonUnitalRing.toNonUnitalNonAssocRing BoundedContinuousFunction.instNonUnitalRing SetLike.instMembership TwoSidedIdeal.setLike compactlySupported HasCompactSupport MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNormedRing.toNonUnitalRing DFunLike.coe BoundedContinuousFunction.instFunLike	—	TwoSidedIdeal.mem_mk' HasCompactSupport.zero HasCompactSupport.add HasCompactSupport.neg HasCompactSupport.mul_left HasCompactSupport.mul_right
norm_lt_iff_of_compactlySupported 📖	mathematical	BoundedContinuousFunction NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing TwoSidedIdeal NonUnitalRing.toNonUnitalNonAssocRing BoundedContinuousFunction.instNonUnitalRing SetLike.instMembership TwoSidedIdeal.setLike compactlySupported Real Real.instLT Real.instZero	Norm.norm BoundedContinuousFunction.instNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNorm DFunLike.coe BoundedContinuousFunction.instFunLike	—	lt_of_le_of_lt BoundedContinuousFunction.norm_coe_le_norm isEmpty_or_nonempty BoundedContinuousFunction.norm_eq_zero_of_empty exist_norm_eq
norm_lt_iff_of_nonempty_compactlySupported 📖	mathematical	BoundedContinuousFunction NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing TwoSidedIdeal NonUnitalRing.toNonUnitalNonAssocRing BoundedContinuousFunction.instNonUnitalRing SetLike.instMembership TwoSidedIdeal.setLike compactlySupported	Real Real.instLT Norm.norm BoundedContinuousFunction.instNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNorm DFunLike.coe BoundedContinuousFunction.instFunLike	—	lt_or_ge norm_lt_iff_of_compactlySupported LT.lt.not_ge LT.lt.trans_le norm_nonneg
ofCompactSupport_mem 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing HasCompactSupport MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	BoundedContinuousFunction TwoSidedIdeal BoundedContinuousFunction.instNonUnitalRing SetLike.instMembership TwoSidedIdeal.setLike compactlySupported ofCompactSupport	—	mem_compactlySupported

---

← Back to Index