Continuous

📁 Source: Mathlib/MeasureTheory/Function/LpSpace/DomAct/Continuous.lean

Statistics

Metric	Count
Definitions	0
Theorems instContinuousSMulDomMulAct, instContinuousVAddDomAddAct	2
Total	2

MeasureTheory.Lp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContinuousSMulDomMulAct 📖	mathematical	—	ContinuousSMul DomMulAct MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp DomMulAct.instSMulSubtypeAEEqFunMemAddSubgroupLp MeasurableSMul.toMeasurableConstSMul ContinuousSMul.toMeasurableSMul DomMulAct.instTopologicalSpace instNormedAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasurableSMul.toMeasurableConstSMul ContinuousSMul.toMeasurableSMul ContinuousSMul.continuous_smul continuous_induced_dom Continuous.compMeasurePreservingLp continuous_snd ContinuousMap.continuous Fact.out
instContinuousVAddDomAddAct 📖	mathematical	—	ContinuousVAdd DomAddAct MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp DomAddAct.instVAddSubtypeAEEqFunMemAddAddSubgroupLp MeasurableVAdd.toMeasurableConstVAdd ContinuousVAdd.toMeasurableVAdd DomAddAct.instTopologicalSpace instNormedAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasurableVAdd.toMeasurableConstVAdd ContinuousVAdd.toMeasurableVAdd ContinuousVAdd.continuous_vadd continuous_induced_dom Continuous.compMeasurePreservingLp continuous_snd ContinuousMap.continuous Fact.out

---

← Back to Index