AEMeasurableOrder

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

Statistics

Metric	Count
Definitions	0
Theorems aemeasurable_of_exist_almost_disjoint_supersets, aemeasurable_of_exist_almost_disjoint_supersets	2
Total	2

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_of_exist_almost_disjoint_supersets 📖	mathematical	MeasurableSet Set Set.instHasSubset setOf ENNReal Preorder.toLT PartialOrder.toPreorder instPartialOrder ofNNReal DFunLike.coe MeasureTheory.Measure MeasureTheory.Measure.instFunLike Set.instInter instZeroENNReal	AEMeasurable measurableSpace	—	exists_countable_dense_no_zero_top MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets instDenselyOrdered instOrderTopology instSecondCountableTopology borelSpace CanLift.prf canLift coe_lt_coe

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_of_exist_almost_disjoint_supersets 📖	mathematical	Dense MeasurableSet Set Set.instHasSubset setOf Preorder.toLT PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice DFunLike.coe Measure ENNReal Measure.instFunLike Set.instInter instZeroENNReal	AEMeasurable	—	MeasurableSet.univ Set.subset_univ MeasurableSet.biInter Set.Countable.mono Set.inter_subset_left Measurable.iInf Encodable.countable Measurable.piecewise measurable_const LE.le.trans measure_iUnion_le Measure.instOuterMeasureClass ENNReal.tsum_le_tsum Set.Countable.to_subtype Summable.tsum_le_tsum ENNReal.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology SummationFilter.instNeBotUnconditional measure_mono Set.inter_subset_inter Set.biInter_subset_of_mem subset_refl Set.instReflSubset ENNReal.summable tsum_zero le_antisymm bot_le Set.ext Filter.mp_mem Filter.univ_mem' iInf_eq_of_forall_ge_of_forall_gt_exists_lt Set.piecewise_eq_of_mem Mathlib.Tactic.Contrapose.contrapose₂ dense_iff_inter_open isOpen_Ioo Set.nonempty_Ioo Set.mem_iUnion Set.piecewise_eq_of_notMem Set.mem_biInter

---

← Back to Index