ContinuousMapDense

📁 Source: Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

Statistics

Metric	Count
Definitions	0
Theorems toLp_denseRange, toLp_denseRange, exists_boundedContinuous_integral_sub_le, exists_boundedContinuous_lintegral_sub_le, exists_hasCompactSupport_integral_sub_le, exists_hasCompactSupport_lintegral_sub_le, boundedContinuousFunction_dense, boundedContinuousFunction_topologicalClosure, exists_boundedContinuous_eLpNorm_sub_le, exists_boundedContinuous_integral_rpow_sub_le, exists_hasCompactSupport_eLpNorm_sub_le, exists_hasCompactSupport_integral_rpow_sub_le, exists_continuous_eLpNorm_sub_le_of_closed	13
Total	13

BoundedContinuousFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLp_denseRange 📖	mathematical	—	DenseRange 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 MeasureTheory.Lp.instNormedAddCommGroup BoundedContinuousFunction DFunLike.coe ContinuousLinearMap Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring instPseudoMetricSpace instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instBoundedAddOfLipschitzAdd AddCommMonoid.toAddMonoid SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd instModule SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing MeasureTheory.Lp.instModule ContinuousLinearMap.funLike toLp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd RingHomSurjective.ids range_toLp MeasureTheory.Lp.boundedContinuousFunction_dense

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLp_denseRange 📖	mathematical	—	DenseRange 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 MeasureTheory.Lp.instNormedAddCommGroup ContinuousMap DFunLike.coe ContinuousLinearMap Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring compactOpen instAddCommMonoidOfContinuousAdd ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsTopologicalAddGroup.toContinuousAdd module 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 NormedAddCommGroup.toAddCommGroup MeasureTheory.Lp.instModule ContinuousLinearMap.funLike toLp	—	Dense.mono SeminormedAddCommGroup.toIsTopologicalAddGroup instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul Set.range_subset_iff BoundedContinuousFunction.toLp_denseRange

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_continuous_eLpNorm_sub_le_of_closed 📖	mathematical	IsOpen Set Set.instHasSubset	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Function.support MemLp	—	exists_eLpNorm_indicator_le ENNReal.coe_lt_coe MeasurableSet.exists_isOpen_diff_lt IsClosed.measurableSet BorelSpace.opensMeasurable LT.lt.ne' Set.subset_inter LE.le.trans_lt measure_mono Measure.instOuterMeasureClass Set.inter_subset_right exists_continuous_zero_one_of_isClosed IsOpen.isClosed_compl IsOpen.inter disjoint_compl_left_iff Real.norm_eq_abs abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_smul NormedSpace.toNormSMulClass mul_le_of_le_one_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg Set.diff_union_of_subset Set.indicator_of_notMem sub_zero Set.indicator_of_mem one_smul sub_self norm_zero zero_smul Function.support_subset_iff' MemLp.smul NormedSpace.toIsBoundedSMul memLp_top_const Continuous.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal ContinuousMap.continuous eLpNorm_indicator_const_le enorm_one NormedDivisionRing.to_normOneClass one_div one_mul IsOrderedRing.toPosMulMono LT.lt.ne PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing eLpNorm_mono CStarRing.norm_one instCStarRingReal Real.instNontrivial abs_zero covariant_swap_add_of_covariant_add ENNReal.HolderTriple.instInfty Continuous.smul IsBoundedSMul.continuousSMul ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass continuous_const LE.le.trans Set.diff_subset_diff Set.Subset.rfl LT.lt.le HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_left

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_boundedContinuous_integral_sub_le 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Real Real.instLT Real.instZero	Real.instLE MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe BoundedContinuousFunction BoundedContinuousFunction.instFunLike	—	ENNReal.ofReal_one Real.rpow_one MeasureTheory.MemLp.exists_boundedContinuous_integral_rpow_sub_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
exists_boundedContinuous_lintegral_sub_le 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral ENorm.enorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe BoundedContinuousFunction BoundedContinuousFunction.instFunLike	—	MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le ENNReal.one_ne_top
exists_hasCompactSupport_integral_sub_le 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Real Real.instLT Real.instZero	HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instLE MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Continuous	—	ENNReal.ofReal_one Real.rpow_one MeasureTheory.MemLp.exists_hasCompactSupport_integral_rpow_sub_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
exists_hasCompactSupport_lintegral_sub_le 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral ENorm.enorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Continuous	—	MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le ENNReal.one_ne_top

MeasureTheory.Lp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boundedContinuousFunction_dense 📖	mathematical	—	Dense 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 instNormedAddCommGroup SetLike.coe AddSubgroup.toAddGroup boundedContinuousFunction	—	SeminormedAddCommGroup.toIsTopologicalAddGroup mem_closure_iff_nhds_basis Metric.nhds_basis_closedEBall MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le memLp LT.lt.ne' Metric.mem_closedEBall' toLp_coeFn edist_toLp_toLp
boundedContinuousFunction_topologicalClosure 📖	mathematical	—	AddSubgroup.topologicalClosure 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 instNormedAddCommGroup AddSubgroup.toAddGroup boundedContinuousFunction Top.top AddSubgroup.instTop	—	SetLike.ext' SeminormedAddCommGroup.toIsTopologicalAddGroup Dense.closure_eq boundedContinuousFunction_dense

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_boundedContinuous_eLpNorm_sub_le 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe BoundedContinuousFunction BoundedContinuousFunction.instFunLike	—	induction_dense MeasureTheory.exists_Lp_half MeasureTheory.exists_eLpNorm_indicator_le LT.lt.ne' ENNReal.coe_pos MeasurableSet.exists_isClosed_diff_lt BorelSpace.opensMeasurable LT.lt.ne LE.le.trans_lt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.eLpNorm_neg neg_sub Set.indicator_diff LT.lt.le MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closed MeasureTheory.Measure.WeaklyRegular.toOuterRegular isOpen_univ Set.subset_univ sub_add_sub_cancel MeasureTheory.AEStronglyMeasurable.sub SeminormedAddCommGroup.toIsTopologicalAddGroup aestronglyMeasurable MeasureTheory.AEStronglyMeasurable.indicator MeasureTheory.aestronglyMeasurable_const IsClosed.measurableSet BoundedContinuousFunction.isBounded_range Continuous.add IsTopologicalAddGroup.toContinuousAdd add Metric.isBounded_range_iff instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd
exists_boundedContinuous_integral_rpow_sub_le 📖	mathematical	Real Real.instLT Real.instZero MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal.ofReal	Real.instLE MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Real.instPow Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe BoundedContinuousFunction BoundedContinuousFunction.instFunLike	—	Real.rpow_pos_of_pos exists_boundedContinuous_eLpNorm_sub_le ENNReal.coe_ne_top Real.rpow_le_rpow_iff MeasureTheory.integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.rpow_nonneg norm_nonneg LT.lt.le inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono ENNReal.toReal_ofReal one_div ENNReal.ofReal_le_ofReal_iff eLpNorm_eq_integral_rpow_norm sub
exists_hasCompactSupport_eLpNorm_sub_le 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Continuous	—	induction_dense MeasureTheory.exists_Lp_half MeasureTheory.exists_eLpNorm_indicator_le LT.lt.ne' ENNReal.coe_pos MeasurableSet.exists_isCompact_isClosed_diff_lt MeasureTheory.Measure.Regular.instInnerRegularCompactLTTop LT.lt.ne LE.le.trans_lt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.eLpNorm_neg neg_sub Set.indicator_diff LT.lt.le exists_compact_superset MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closed MeasureTheory.Measure.WeaklyRegular.toOuterRegular MeasureTheory.Measure.Regular.weaklyRegular isOpen_interior sub_add_sub_cancel MeasureTheory.AEStronglyMeasurable.sub SeminormedAddCommGroup.toIsTopologicalAddGroup aestronglyMeasurable MeasureTheory.AEStronglyMeasurable.indicator MeasureTheory.aestronglyMeasurable_const IsClosed.measurableSet BorelSpace.opensMeasurable HasCompactSupport.intro Function.notMem_support Mathlib.Tactic.Contrapose.contrapose₄ interior_subset Continuous.add IsTopologicalAddGroup.toContinuousAdd add HasCompactSupport.add
exists_hasCompactSupport_integral_rpow_sub_le 📖	mathematical	Real Real.instLT Real.instZero MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal.ofReal	HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instLE MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Real.instPow Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Continuous	—	Real.rpow_pos_of_pos exists_hasCompactSupport_eLpNorm_sub_le ENNReal.coe_ne_top Real.rpow_le_rpow_iff MeasureTheory.integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.rpow_nonneg norm_nonneg LT.lt.le inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono ENNReal.toReal_ofReal one_div ENNReal.ofReal_le_ofReal_iff eLpNorm_eq_integral_rpow_norm sub

---

← Back to Index