SubFinite

📁 Source: Mathlib/MeasureTheory/Measure/SubFinite.lean

Statistics

Metric	Count
Definitions	0
Theorems sub_le_iff_le_add, withDensity_sub, withDensity_sub_of_le	3
Total	3

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sub_le_iff_le_add 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder instSub instAdd	—	MeasureTheory.exists_isHahnDecomposition LE.le.trans MeasureTheory.IsHahnDecomposition.le_on le_add_left le_rfl sub_le_iff_le_add_of_le MeasureTheory.isFiniteMeasureRestrict MeasureTheory.IsHahnDecomposition.ge_on_compl restrict_sub_eq_restrict_sub_restrict MeasurableSet.compl MeasureTheory.IsHahnDecomposition.measurableSet restrict_mono subset_rfl Set.instReflSubset restrict_add_restrict_compl add_le_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LE.le.trans_eq Mathlib.Tactic.Abel.subst_into_add Mathlib.Tactic.Abel.term_atom Mathlib.Tactic.Abel.term_add_const zero_add Mathlib.Tactic.Abel.const_add_term sub_le_of_le_add
withDensity_sub 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	withDensity Pi.instSub ENNReal.instSub MeasureTheory.Measure instSub	—	le_antisymm measurableSet_le BorelSpace.opensMeasurable ENNReal.borelSpace OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology ENNReal.instSecondCountableTopology restrict_add_restrict_compl MeasureTheory.withDensity_apply instOuterMeasureClass MeasureTheory.lintegral_eq_zero_iff Measurable.sub' ENNReal.instMeasurableSub₂ Measurable.fun_comp Measurable.snd measurable_id' MeasureTheory.ae_restrict_of_forall_mem ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub zero_add restrict_sub_eq_restrict_sub_restrict MeasurableSet.compl MeasureTheory.restrict_withDensity MeasureTheory.isFiniteMeasureRestrict withDensity_sub_of_le LT.lt.le le_refl LE.le.trans le_add_left le_rfl sub_le_of_le_add MeasureTheory.withDensity_add_right MeasureTheory.withDensity_mono MeasureTheory.ae_of_all le_tsub_add
withDensity_sub_of_le 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass	withDensity Pi.instSub ENNReal.instSub instSub	—	instOuterMeasureClass ext sub_apply MeasureTheory.withDensity_mono MeasureTheory.withDensity_apply MeasureTheory.lintegral_sub MeasureTheory.ae_restrict_of_ae

---

← Back to Index