Basic

📁 Source: Mathlib/MeasureTheory/OuterMeasure/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems coe_fn_injective, ext, ext_iff, ext_nonempty, iUnion_nat_of_monotone_of_tsum_ne_top, iUnion_of_tendsto_zero, exists_mem_forall_mem_nhdsWithin_pos_measure, measure_biUnion_finset_le, measure_biUnion_le, measure_biUnion_null_iff, measure_diff_null, measure_empty, measure_eq_top_mono, measure_iUnion_fintype_le, measure_iUnion_le, measure_iUnion_null, measure_iUnion_null_iff, measure_iUnion_of_tendsto_zero, measure_le_inter_add_diff, measure_lt_top_mono, measure_mono, measure_mono_null, measure_null_iff_singleton, measure_null_of_locally_null, measure_pos_of_superset, measure_sUnion_null_iff, measure_union_le, measure_union_null, measure_union_null_iff, measure_univ_le_add_compl, pos_mono	31
Total	31

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mem_forall_mem_nhdsWithin_pos_measure 📖	mathematical	—	Set Set.instMembership ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe	—	Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq Mathlib.Tactic.Push.not_forall_eq measure_null_of_locally_null ENNReal.instCanonicallyOrderedAdd
measure_biUnion_finset_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Set Set.iUnion Finset Finset.instMembership Finset.sum ENNReal.instAddCommMonoid	—	LE.le.trans_eq measure_biUnion_le Finset.countable_toSet Finset.tsum_subtype
measure_biUnion_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Set Set.iUnion Set.instMembership tsum Set.Elem ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	Set.Countable.to_subtype Set.biUnion_eq_iUnion measure_iUnion_le
measure_biUnion_null_iff 📖	mathematical	—	DFunLike.coe Set ENNReal Set.iUnion Set.instMembership instZeroENNReal	—	measure_mono_null Set.subset_biUnion_of_mem Set.Countable.to_subtype Set.iUnion_coe_set Set.iUnion_congr_Prop tsum_zero ENNReal.instCanonicallyOrderedAdd measure_iUnion_le
measure_diff_null 📖	mathematical	DFunLike.coe Set ENNReal instZeroENNReal	Set.instSDiff	—	LE.le.antisymm measure_mono Set.diff_subset measure_le_inter_add_diff add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid Set.inter_subset_right zero_add
measure_empty 📖	mathematical	—	DFunLike.coe Set ENNReal Set.instEmptyCollection instZeroENNReal	—	OuterMeasureClass.measure_empty
measure_eq_top_mono 📖	—	Set Set.instHasSubset DFunLike.coe ENNReal Top.top instTopENNReal	—	—	eq_top_mono measure_mono
measure_iUnion_fintype_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Set Set.iUnion Finset.sum ENNReal.instAddCommMonoid Finset.univ	—	Set.iUnion_congr_Prop Set.iUnion_true measure_biUnion_finset_le
measure_iUnion_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Set Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	rel_iSup_tsum measure_empty iUnion_disjointed OuterMeasureClass.measure_iUnion_nat_le disjoint_disjointed Summable.tsum_le_tsum ENNReal.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology SummationFilter.instNeBotUnconditional measure_mono disjointed_subset ENNReal.summable
measure_iUnion_null 📖	mathematical	DFunLike.coe Set ENNReal instZeroENNReal	Set.iUnion	—	measure_iUnion_null_iff
measure_iUnion_null_iff 📖	mathematical	—	DFunLike.coe Set ENNReal Set.iUnion instZeroENNReal	—	Set.sUnion_range measure_sUnion_null_iff Set.countable_range Set.forall_mem_range
measure_iUnion_of_tendsto_zero 📖	mathematical	Filter.Tendsto ENNReal DFunLike.coe Set Set.instSDiff Set.iUnion nhds ENNReal.instTopologicalSpace instZeroENNReal	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	le_antisymm measure_le_inter_add_diff add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid measure_mono Set.inter_subset_right le_iSup add_zero Filter.Tendsto.add ENNReal.instContinuousAdd tendsto_const_nhds ge_of_tendsto' instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology iSup_le Set.subset_iUnion
measure_le_inter_add_diff 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Set Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Set.instInter Set.instSDiff	—	Set.inter_union_diff measure_union_le
measure_lt_top_mono 📖	—	Set Set.instHasSubset ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Top.top instTopENNReal	—	—	LE.le.trans_lt measure_mono
measure_mono 📖	mathematical	Set Set.instHasSubset	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe	—	OuterMeasureClass.measure_mono
measure_mono_null 📖	—	Set Set.instHasSubset DFunLike.coe ENNReal instZeroENNReal	—	—	eq_bot_mono measure_mono
measure_null_iff_singleton 📖	mathematical	—	DFunLike.coe Set ENNReal instZeroENNReal Set.instSingletonSet	—	measure_biUnion_null_iff Set.biUnion_of_singleton
measure_null_of_locally_null 📖	—	Set Filter Filter.instMembership nhdsWithin DFunLike.coe ENNReal instZeroENNReal	—	—	measure_mono_null measure_biUnion_null_iff TopologicalSpace.countable_cover_nhdsWithin Function.sometimes_spec
measure_pos_of_superset 📖	mathematical	Set Set.instHasSubset	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe	—	LT.lt.trans_le Ne.bot_lt measure_mono
measure_sUnion_null_iff 📖	mathematical	—	DFunLike.coe Set ENNReal Set.sUnion instZeroENNReal	—	Set.sUnion_eq_biUnion measure_biUnion_null_iff
measure_union_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Set Set.instUnion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Set.union_eq_iUnion Finset.sum_insert Finset.sum_singleton measure_iUnion_fintype_le
measure_union_null 📖	mathematical	DFunLike.coe Set ENNReal instZeroENNReal	Set.instUnion	—	—
measure_union_null_iff 📖	mathematical	—	DFunLike.coe Set ENNReal Set.instUnion instZeroENNReal	—	Set.union_eq_iUnion Bool.countable
measure_univ_le_add_compl 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Set Set.univ Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Compl.compl Set.instCompl	—	measure_union_le Set.union_compl_self
pos_mono 📖	—	Set Set.instHasSubset ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe	—	—	LT.lt.trans_le measure_mono

MeasureTheory.OuterMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_fn_injective 📖	mathematical	—	MeasureTheory.OuterMeasure DFunLike.coe Set ENNReal instFunLikeSetENNReal	—	DFunLike.coe_injective
ext 📖	—	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal instFunLikeSetENNReal	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal instFunLikeSetENNReal	—	ext
ext_nonempty 📖	—	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal instFunLikeSetENNReal	—	—	ext Set.eq_empty_or_nonempty MeasureTheory.measure_empty instOuterMeasureClass
iUnion_nat_of_monotone_of_tsum_ne_top 📖	mathematical	Set Set.instHasSubset	DFunLike.coe MeasureTheory.OuterMeasure ENNReal instFunLikeSetENNReal Set.iUnion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	MeasureTheory.measure_iUnion_of_tendsto_zero instOuterMeasureClass Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_nhds_bot_mono' ENNReal.instOrderTopology ENNReal.tendsto_sum_nat_add LE.le.trans mono monotone_nat_of_le_succ le_or_gt Set.mem_iUnion le_refl MeasureTheory.measure_iUnion_le instCountableNat
iUnion_of_tendsto_zero 📖	mathematical	Filter.Tendsto ENNReal DFunLike.coe MeasureTheory.OuterMeasure Set instFunLikeSetENNReal Set.instSDiff Set.iUnion nhds ENNReal.instTopologicalSpace instZeroENNReal	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	MeasureTheory.measure_iUnion_of_tendsto_zero instOuterMeasureClass

---

← Back to Index