UpperLower

📁 Source: Mathlib/MeasureTheory/Order/UpperLower.lean

Statistics

Metric	Count
Definitions	0
Theorems volume_eq_zero, null_frontier, null_frontier, nullMeasurableSet, null_frontier	5
Total	5

IsAntichain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
volume_eq_zero 📖	mathematical	IsAntichain Pi.hasLe Real Real.instLE	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume instZeroENNReal	—	MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass closure_diff_interior interior_eq_empty Pi.instNeBotNhdsWithinIio nhdsLT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Set.diff_empty subset_closure Set.OrdConnected.null_frontier ordConnected

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
null_frontier 📖	mathematical	IsLowerSet Pi.hasLe Real Real.instLE	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instZeroENNReal	—	MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass Set.indicator_of_mem IsUpperSet.exists_subset_ball compl frontier_subset_closure frontier_compl Set.indicator_of_notMem exists_subset_ball Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet Pi.borelSpace Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace TopologicalSpace.instSecondCountableTopologyForallOfCountable Besicovitch.instHasBesicovitchCovering FiniteDimensional.finiteDimensional_pi' FiniteDimensional.rclike_to_real MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Real.locallyFinite_volume IsClosed.measurableSet Pi.opensMeasurableSpace BorelSpace.opensMeasurable isClosed_closure

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
null_frontier 📖	mathematical	IsUpperSet Pi.hasLe Real Real.instLE	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instZeroENNReal	—	MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass Set.indicator_of_mem IsLowerSet.exists_subset_ball compl frontier_subset_closure frontier_compl Set.indicator_of_notMem exists_subset_ball Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet Pi.borelSpace Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace TopologicalSpace.instSecondCountableTopologyForallOfCountable Besicovitch.instHasBesicovitchCovering FiniteDimensional.finiteDimensional_pi' FiniteDimensional.rclike_to_real MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Real.locallyFinite_volume IsClosed.measurableSet Pi.opensMeasurableSpace BorelSpace.opensMeasurable isClosed_closure

Set.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nullMeasurableSet 📖	mathematical	—	MeasureTheory.NullMeasurableSet MeasurableSpace.pi Real Real.measurableSpace MeasureTheory.MeasureSpace.volume MeasureTheory.MeasureSpace.pi Real.measureSpace	—	nullMeasurableSet_of_null_frontier Pi.opensMeasurableSpace Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace null_frontier
null_frontier 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instZeroENNReal	—	upperClosure_inter_lowerClosure MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass frontier_inter_subset MeasureTheory.measure_union_null MeasureTheory.measure_inter_null_of_null_left IsUpperSet.null_frontier UpperSet.upper MeasureTheory.measure_inter_null_of_null_right IsLowerSet.null_frontier LowerSet.lower

---

← Back to Index