Regular

📁 Source: Mathlib/MeasureTheory/Integral/Regular.lean

Statistics

Metric	Count
Definitions	0
Theorems measure_eq_biInf_integral_hasCompactSupport, measure_eq_biSup_integral_continuous	2
Total	2

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measure_eq_biInf_integral_hasCompactSupport 📖	mathematical	IsCompact	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace HasCompactSupport Real.instZero Set.EqOn Pi.instOne Real.instOne Pi.hasLe Real.instLE Pi.instZero ENNReal.ofReal MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	le_antisymm MeasureTheory.Integrable.measure_le_integral Continuous.integrable_of_hasCompactSupport BorelSpace.opensMeasurable Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass le_of_forall_gt exists_isOpen_lt_of_lt MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts instWeaklyLocallyCompactSpaceOfLocallyCompactSpace instR1Space exists_continuous_one_zero_of_isCompact IsOpen.isClosed_compl Set.disjoint_compl_right_iff_subset LE.le.trans_lt MeasureTheory.integral_le_measure Eq.le

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measure_eq_biSup_integral_continuous 📖	mathematical	IsOpen	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.EqOn Pi.instZero Real.instZero Compl.compl Set.instCompl Pi.hasLe Real.instLE Pi.instOne Real.instOne ENNReal.ofReal MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	le_antisymm le_of_forall_lt MeasurableSet.exists_lt_isCompact_of_ne_top measurableSet BorelSpace.opensMeasurable exists_continuous_zero_one_of_isClosed isClosed_compl IsCompact.isClosed Set.disjoint_compl_left_iff_subset LT.lt.trans_le MeasureTheory.Integrable.measure_le_integral MeasureTheory.Integrable.of_mem_Icc Continuous.aemeasurable Real.borelSpace Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass Eq.ge MeasureTheory.integral_le_measure le_of_eq

---

← Back to Index