ContinuousLinearMap

📁 Source: Mathlib/MeasureTheory/Constructions/BorelSpace/ContinuousLinearMap.lean

Statistics

Metric	Count
Definitions instMeasurableSpace	1
Theorems apply_continuousLinearMap, instBorelSpace, measurable, measurable_apply, measurable_apply', measurable_coe, measurable_comp, apply_continuousLinearMap, aemeasurable_smul_const, measurable_smul_const	10
Total	11

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_continuousLinearMap 📖	mathematical	AEMeasurable ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.instMeasurableSpace	DFunLike.coe ContinuousLinearMap.funLike	—	Measurable.comp_aemeasurable RingHomIsometric.ids smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.measurable BorelSpace.opensMeasurable ContinuousLinearMap.instBorelSpace

ContinuousLinearMap

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	7 math math: measurable_apply₂, MeasureTheory.aemeasurable_fderivWithin, measurable_apply, measurable_coe, measurable_fderiv_with_param, measurable_fderiv, instBorelSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instBorelSpace 📖	mathematical	—	BorelSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instMeasurableSpace	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
measurable 📖	mathematical	—	Measurable DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup funLike	—	Continuous.measurable continuous
measurable_apply 📖	mathematical	—	Measurable ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instMeasurableSpace DFunLike.coe funLike	—	Continuous.measurable SeminormedAddCommGroup.toIsTopologicalAddGroup BorelSpace.opensMeasurable instBorelSpace IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul continuous
measurable_apply' 📖	mathematical	—	Measurable MeasurableSpace.pi ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DFunLike.coe funLike	—	measurable_pi_lambda measurable
measurable_coe 📖	mathematical	—	Measurable ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instMeasurableSpace MeasurableSpace.pi DFunLike.coe funLike	—	measurable_pi_lambda measurable_apply
measurable_comp 📖	mathematical	Measurable	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup funLike	—	Measurable.comp measurable

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_continuousLinearMap 📖	mathematical	Measurable ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.instMeasurableSpace	DFunLike.coe ContinuousLinearMap.funLike	—	comp RingHomIsometric.ids smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.measurable BorelSpace.opensMeasurable ContinuousLinearMap.instBorelSpace

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_smul_const 📖	mathematical	—	AEMeasurable SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule	—	MeasurableEmbedding.aemeasurable_comp_iff Topology.IsClosedEmbedding.measurableEmbedding isClosedEmbedding_smul_left SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
measurable_smul_const 📖	mathematical	—	Measurable SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule	—	MeasurableEmbedding.measurable_comp_iff Topology.IsClosedEmbedding.measurableEmbedding isClosedEmbedding_smul_left SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace

---

← Back to Index