Support

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

Statistics

Metric	Count
Definitions `support`	1
Theorems `mem_measureSupport`, `notMem_measureSupport`, `support_mono`, `compl_support_eq_sUnion`, `interior_inter_support`, `isClosed_support`, `isOpen_compl_support`, `measure_compl_support`, `mem_support_iff`, `mem_support_iff_forall`, `mem_support_restrict`, `nonempty_inter_support_of_pos`, `nonempty_support`, `nonempty_support_iff`, `notMem_support_iff`, `notMem_support_iff_exists`, `nullMeasurableSet_compl_support`, `nullMeasurableSet_support`, `subset_compl_support_of_isOpen`, `support_add`, `support_eq_forall_isOpen`, `support_eq_sInter`, `support_eq_univ`, `support_mem_ae`, `support_mem_ae_of_isLindelof`, `support_mono`, `support_restrict_subset`, `support_subset_of_isClosed`, `support_zero`	29
Total	30

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_measureSupport` 📖	mathematical	`Filter.HasBasis` `nhds`	`Set` `Set.instMembership` `MeasureTheory.Measure.support` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike`	—	`frequently_smallSets` `MeasureTheory.pos_mono` `MeasureTheory.Measure.instOuterMeasureClass`
`notMem_measureSupport` 📖	mathematical	`Filter.HasBasis` `nhds`	`Set` `Set.instMembership` `MeasureTheory.Measure.support` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal`	—	`mem_measureSupport` `ENNReal.instCanonicallyOrderedAdd`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`support` 📖	CompOp	28 math math: `Filter.HasBasis.notMem_measureSupport`, `nonempty_support_iff`, `nonempty_inter_support_of_pos`, `mem_support_iff`, `notMem_support_iff`, `interior_inter_support`, `nonempty_support`, `compl_support_eq_sUnion`, `measure_compl_support`, `mem_support_iff_forall`, `support_mono`, `notMem_support_iff_exists`, `support_eq_forall_isOpen`, `support_mem_ae`, `mem_support_restrict`, `subset_compl_support_of_isOpen`, `nullMeasurableSet_support`, `isOpen_compl_support`, `support_eq_sInter`, `support_zero`, `nullMeasurableSet_compl_support`, `support_eq_univ`, `isClosed_support`, `Filter.HasBasis.mem_measureSupport`, `support_subset_of_isClosed`, `support_add`, `support_restrict_subset`, `AbsolutelyContinuous.support_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_support_eq_sUnion` 📖	mathematical	—	`Compl.compl` `Set` `Set.instCompl` `support` `Set.sUnion` `setOf` `IsOpen` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `instFunLike` `instZeroENNReal`	—	`Set.ext` `Filter.HasBasis.notMem_measureSupport` `nhds_basis_opens`
`interior_inter_support` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.instInter` `interior` `support` `restrict`	—	`mem_support_restrict` `Filter.HasBasis.frequently_smallSets` `nhdsWithin_basis_open` `MeasureTheory.pos_mono` `instOuterMeasureClass` `LT.lt.trans_le` `Filter.HasBasis.mem_measureSupport` `nhds_basis_opens` `IsOpen.inter` `isOpen_interior` `MeasureTheory.measure_mono` `Set.inter_subset_inter` `subset_refl` `Set.instReflSubset` `interior_subset`
`isClosed_support` 📖	mathematical	—	`IsClosed` `support`	—	`Filter.HasBasis.mem_measureSupport` `nhds_basis_opens` `Filter.HasBasis.frequently_iff`
`isOpen_compl_support` 📖	mathematical	—	`IsOpen` `Compl.compl` `Set` `Set.instCompl` `support`	—	`isOpen_compl_iff` `isClosed_support`
`measure_compl_support` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Compl.compl` `Set.instCompl` `support` `instZeroENNReal`	—	`support_mem_ae`
`mem_support_iff` 📖	mathematical	—	`Set` `Set.instMembership` `support` `Filter.Frequently` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `instFunLike` `Filter.smallSets` `nhds`	—	—
`mem_support_iff_forall` 📖	mathematical	—	`Set` `Set.instMembership` `support` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `instFunLike`	—	`Filter.HasBasis.mem_measureSupport` `Filter.basis_sets`
`mem_support_restrict` 📖	mathematical	—	`Set` `Set.instMembership` `support` `restrict` `Filter.Frequently` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `instFunLike` `Filter.smallSets` `nhdsWithin`	—	`Filter.HasBasis.mem_measureSupport` `nhds_basis_opens` `Filter.HasBasis.frequently_smallSets` `nhdsWithin_basis_open` `MeasureTheory.pos_mono` `instOuterMeasureClass`
`nonempty_inter_support_of_pos` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike`	`Set.Nonempty` `Set.instInter` `support`	—	`Set.not_disjoint_iff_nonempty_inter` `Mathlib.Tactic.Contrapose.contrapose₃` `LE.le.trans` `MeasureTheory.OuterMeasure.mono` `Disjoint.subset_compl_right` `measure_compl_support`
`nonempty_support` 📖	mathematical	—	`Set.Nonempty` `support`	—	`Set.Nonempty.right` `nonempty_inter_support_of_pos` `measure_univ_pos`
`nonempty_support_iff` 📖	mathematical	—	`Set.Nonempty` `support`	—	`Set.not_nonempty_iff_eq_empty` `support_zero` `nonempty_support`
`notMem_support_iff` 📖	mathematical	—	`Set` `Set.instMembership` `support` `Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `instFunLike` `instZeroENNReal` `Filter.smallSets` `nhds`	—	`ENNReal.instCanonicallyOrderedAdd`
`notMem_support_iff_exists` 📖	mathematical	—	`Set` `Set.instMembership` `support` `Filter` `Filter.instMembership` `nhds` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `instFunLike` `instZeroENNReal`	—	`ENNReal.instCanonicallyOrderedAdd`
`nullMeasurableSet_compl_support` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Compl.compl` `Set` `Set.instCompl` `support`	—	`MeasureTheory.NullMeasurableSet.of_null` `measure_compl_support`
`nullMeasurableSet_support` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `support`	—	`MeasureTheory.NullMeasurableSet.compl_iff` `nullMeasurableSet_compl_support`
`subset_compl_support_of_isOpen` 📖	mathematical	`IsOpen` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `instZeroENNReal`	`Set.instHasSubset` `Compl.compl` `Set.instCompl` `support`	—	`notMem_support_iff_exists` `IsOpen.mem_nhds`
`support_add` 📖	mathematical	—	`support` `MeasureTheory.Measure` `instAdd` `Set` `Set.instUnion`	—	`Set.ext` `ENNReal.instCanonicallyOrderedAdd`
`support_eq_forall_isOpen` 📖	mathematical	—	`support` `setOf`	—	`Filter.HasBasis.mem_measureSupport` `nhds_basis_opens`
`support_eq_sInter` 📖	mathematical	—	`support` `Set.sInter` `setOf` `Set` `IsClosed` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `instFunLike` `Compl.compl` `Set.instCompl` `instZeroENNReal`	—	`compl_compl` `Set.compl_sUnion` `Function.Involutive.image_eq_preimage_symm` `compl_involutive` `compl_support_eq_sUnion`
`support_eq_univ` 📖	mathematical	—	`support` `Set.univ`	—	`measure_pos_of_mem_nhds`
`support_mem_ae` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `support`	—	`support_mem_ae_of_isLindelof` `HereditarilyLindelofSpace.isLindelof`
`support_mem_ae_of_isLindelof` 📖	mathematical	`IsLindelof` `Compl.compl` `Set` `Set.instCompl` `support`	`Filter` `Filter.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	—	`instOuterMeasureClass` `IsLindelof.compl_mem_sets_of_nhdsWithin` `MeasureTheory.instCountableInterFilter` `IsOpen.nhdsWithin_eq` `isOpen_compl_support` `notMem_support_iff_exists` `compl_compl`
`support_mono` 📖	mathematical	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Set` `Set.instHasSubset` `support`	—	`AbsolutelyContinuous.support_mono` `LE.le.absolutelyContinuous`
`support_restrict_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `support` `restrict` `Set.instInter` `closure`	—	`Set.subset_inter` `support_subset_of_isClosed` `isClosed_closure` `instOuterMeasureClass` `MeasureTheory.mem_ae_iff` `restrict_apply` `IsOpen.measurableSet` `IsClosed.isOpen_compl` `Disjoint.eq_bot` `HasSubset.Subset.disjoint_compl_left` `subset_closure` `MeasureTheory.OuterMeasure.empty` `support_mono` `restrict_le_self`
`support_subset_of_isClosed` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	`Set.instHasSubset` `support`	—	`instOuterMeasureClass` `Set.compl_subset_compl` `subset_compl_support_of_isOpen` `IsClosed.isOpen_compl`
`support_zero` 📖	mathematical	—	`support` `MeasureTheory.Measure` `instZero` `Set` `Set.instEmptyCollection`	—	—

MeasureTheory.Measure.AbsolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`support_mono` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`Set` `Set.instHasSubset` `MeasureTheory.Measure.support`	—	`Filter.Frequently.mp` `Filter.Eventually.of_forall` `pos_mono`

---

← Back to Index