UnitInterval

📁 Source: Mathlib/MeasureTheory/Constructions/UnitInterval.lean

Statistics

Metric	Count
Definitions instMeasureSpaceElemReal, symmMeasurableEquiv	2
Theorems coe_symmMeasurableEquiv, instIsProbabilityMeasureElemRealVolume, instNoAtomsElemRealVolume, measurableEmbedding_coe, measurable_symm, measurePreserving_coe, measurePreserving_symm, symmMeasurableEquiv_apply, symmMeasurableEquiv_symm_apply, symm_symmMeasurableEquiv, volume_Icc, volume_Ici, volume_Ico, volume_Iic, volume_Iio, volume_Ioc, volume_Ioi, volume_Ioo, volume_apply, volume_def, volume_uIcc, volume_uIoc, volume_uIoo	23
Total	25

unitInterval

Definitions

Name	Category	Theorems
instMeasureSpaceElemReal 📖	CompOp	20 math math: volume_Ioo, volume_Iic, volume_def, measurePreserving_coe, volume_Ico, volume_apply, MeasureTheory.Measure.exists_measurable_map_eq, measurePreserving_symm, volume_uIcc, volume_Ici, volume_uIoo, volume_Icc, ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval, Manifold.riemannianEDist_def, instIsProbabilityMeasureElemRealVolume, volume_Ioc, instNoAtomsElemRealVolume, volume_uIoc, volume_Iio, volume_Ioi
symmMeasurableEquiv 📖	CompOp	4 math math: coe_symmMeasurableEquiv, symmMeasurableEquiv_apply, symmMeasurableEquiv_symm_apply, symm_symmMeasurableEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_symmMeasurableEquiv 📖	mathematical	—	DFunLike.coe MeasurableEquiv Set.Elem Real unitInterval Subtype.instMeasurableSpace Set Set.instMembership Real.measurableSpace EquivLike.toFunLike MeasurableEquiv.instEquivLike symmMeasurableEquiv symm	—	—
instIsProbabilityMeasureElemRealVolume 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal MeasureTheory.MeasureSpace.volume	—	MeasureTheory.Measure.Subtype.volume_univ nullMeasurableSet_Icc BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Real.volume_Icc sub_zero ENNReal.ofReal_one
instNoAtomsElemRealVolume 📖	mathematical	—	MeasureTheory.NoAtoms Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal MeasureTheory.MeasureSpace.volume	—	volume_apply Set.image_singleton MeasureTheory.NoAtoms.measure_singleton Real.noAtoms_volume
measurableEmbedding_coe 📖	mathematical	—	MeasurableEmbedding Real Set Set.instMembership unitInterval Subtype.instMeasurableSpace Real.measurableSpace	—	Subtype.val_injective measurable_subtype_coe MeasurableSet.subtype_image measurableSet_Icc BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
measurable_symm 📖	mathematical	—	Measurable Set.Elem Real unitInterval Subtype.instMeasurableSpace Set Set.instMembership Real.measurableSpace symm	—	Continuous.measurable Subtype.opensMeasurableSpace BorelSpace.opensMeasurable Real.borelSpace Subtype.borelSpace continuous_symm
measurePreserving_coe 📖	mathematical	—	MeasureTheory.MeasurePreserving Real Set Set.instMembership unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Real.measureSpace MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.restrict	—	MeasureTheory.measurePreserving_subtype_coe measurableSet_Icc BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
measurePreserving_symm 📖	mathematical	—	MeasureTheory.MeasurePreserving Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal symm MeasureTheory.MeasureSpace.volume	—	measurable_symm MeasureTheory.Measure.ext MeasurableEquiv.map_apply coe_symmMeasurableEquiv volume_apply image_coe_preimage_symm MeasureTheory.Measure.map_apply Measurable.const_sub ContinuousSub.measurableSub Real.borelSpace IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal measurable_id' MeasurableSet.subtype_image measurableSet_Icc BorelSpace.opensMeasurable HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.MeasurePreserving.map_eq MeasureTheory.Measure.measurePreserving_sub_left ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousNeg.measurableNeg IsSemitopologicalRing.toContinuousNeg MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real locallyCompact_of_proper instProperSpaceReal MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite PseudoEMetricSpace.pseudoMetrizableSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant
symmMeasurableEquiv_apply 📖	mathematical	—	DFunLike.coe MeasurableEquiv Set.Elem Real unitInterval Subtype.instMeasurableSpace Set Set.instMembership Real.measurableSpace EquivLike.toFunLike MeasurableEquiv.instEquivLike symmMeasurableEquiv symm	—	—
symmMeasurableEquiv_symm_apply 📖	mathematical	—	DFunLike.coe MeasurableEquiv Set.Elem Real unitInterval Subtype.instMeasurableSpace Set Set.instMembership Real.measurableSpace EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.symm symmMeasurableEquiv symm	—	—
symm_symmMeasurableEquiv 📖	mathematical	—	MeasurableEquiv.symm Set.Elem Real unitInterval Subtype.instMeasurableSpace Set Set.instMembership Real.measurableSpace symmMeasurableEquiv	—	—
volume_Icc 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.Icc Subtype.preorder Real.instPreorder Set.instMembership ENNReal.ofReal Real.instSub	—	volume_apply Set.image_subtype_val_Icc Set.ordConnected_Icc Real.volume_Icc
volume_Ici 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.Ici Subtype.preorder Real.instPreorder Set.instMembership ENNReal.ofReal Real.instSub Real.instOne	—	volume_apply Set.image_subtype_val_Icc_Ici Real.volume_Icc
volume_Ico 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.Ico Subtype.preorder Real.instPreorder Set.instMembership ENNReal.ofReal Real.instSub	—	volume_apply Set.image_subtype_val_Ico Set.ordConnected_Icc Real.volume_Ico
volume_Iic 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.Iic Subtype.preorder Real.instPreorder Set.instMembership ENNReal.ofReal	—	volume_apply Set.image_subtype_val_Icc_Iic Real.volume_Icc sub_zero
volume_Iio 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.Iio Subtype.preorder Real.instPreorder Set.instMembership ENNReal.ofReal	—	volume_image_subtype_coe measurableSet_Icc BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Set.image_subtype_val_Icc_Iio Real.volume_Ico sub_zero
volume_Ioc 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.Ioc Subtype.preorder Real.instPreorder Set.instMembership ENNReal.ofReal Real.instSub	—	volume_apply Set.image_subtype_val_Ioc Set.ordConnected_Icc Real.volume_Ioc
volume_Ioi 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.Ioi Subtype.preorder Real.instPreorder Set.instMembership ENNReal.ofReal Real.instSub Real.instOne	—	volume_apply Set.image_subtype_val_Icc_Ioi Real.volume_Ioc
volume_Ioo 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.Ioo Subtype.preorder Real.instPreorder Set.instMembership ENNReal.ofReal Real.instSub	—	volume_apply Set.image_subtype_val_Ioo Set.ordConnected_Icc Real.volume_Ioo
volume_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Real.measureSpace Set.image Set.instMembership	—	MeasurableEmbedding.comap_apply measurableEmbedding_coe
volume_def 📖	mathematical	—	MeasureTheory.MeasureSpace.volume Set.Elem Real unitInterval instMeasureSpaceElemReal MeasureTheory.Measure.comap Set Set.instMembership MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace	—	—
volume_uIcc 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.uIcc Set.Icc.lattice Real.instZero Real.instOne Real.lattice EDist.edist PseudoEMetricSpace.toEDist instPseudoEMetricSpaceSubtype Set.instMembership EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace	—	volume_apply Set.image_subtype_val_Icc Set.ordConnected_Icc Real.volume_Icc max_sub_min_eq_abs IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add edist_dist
volume_uIoc 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.uIoc Subtype.instLinearOrder Real.linearOrder Set.instMembership EDist.edist PseudoEMetricSpace.toEDist instPseudoEMetricSpaceSubtype EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace	—	volume_apply Set.image_subtype_val_Ioc Set.ordConnected_Icc Real.volume_Ioc max_sub_min_eq_abs IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add edist_dist
volume_uIoo 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set.Elem Real unitInterval MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceElemReal Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.uIoo Subtype.instLinearOrder Real.linearOrder Set.instMembership EDist.edist PseudoEMetricSpace.toEDist instPseudoEMetricSpaceSubtype EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace	—	volume_apply Set.image_subtype_val_Ioo Set.ordConnected_Icc Real.volume_Ioo max_sub_min_eq_abs IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add edist_dist

---

← Back to Index