Documentation Verification Report

VitaliFamily

📁 Source: Mathlib/MeasureTheory/Covering/VitaliFamily.lean

Statistics

Metric	Count
Definitions `VitaliFamily`, `FineSubfamilyOn`, `covering`, `index`, `enlarge`, `filterAt`, `mono`, `setsAt`	8
Theorems `vitaliFamily`, `covering_disjoint`, `covering_disjoint_subtype`, `covering_mem`, `covering_mem_family`, `exists_disjoint_covering_ae`, `index_countable`, `index_subset`, `measurableSet_u`, `measure_diff_biUnion`, `measure_le_tsum`, `measure_le_tsum_of_absolutelyContinuous`, `covering`, `eventually_filterAt_iff`, `eventually_filterAt_measurableSet`, `eventually_filterAt_mem_setsAt`, `eventually_filterAt_subset_closedBall`, `eventually_filterAt_subset_of_nhds`, `filterAt_basis_closedBall`, `filterAt_enlarge`, `filterAt_neBot`, `fineSubfamilyOn_iff_frequently`, `fineSubfamilyOn_of_frequently`, `frequently_filterAt_iff`, `measurableSet`, `mem_filterAt_iff`, `nonempty_interior`, `nontrivial`, `tendsto_filterAt_iff`	29
Total	37

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vitaliFamily` 📖	mathematical	`Filter.HasBasis` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`Set` `VitaliFamily.filterAt` `setOf` `Set.instMembership` `VitaliFamily.setsAt` `Set.instHasSubset`	—	`inf_principal` `smallSets`

VitaliFamily

Definitions

Name	Category	Theorems
`FineSubfamilyOn` 📖	MathDef	2 math math: `fineSubfamilyOn_of_frequently`, `fineSubfamilyOn_iff_frequently`
`enlarge` 📖	CompOp	1 math math: `filterAt_enlarge`
`filterAt` 📖	CompOp	35 math math: `Filter.HasBasis.vitaliFamily`, `eventually_filterAt_iff`, `ae_tendsto_lintegral_div`, `ae_tendsto_measure_inter_div_of_measurableSet`, `filterAt_basis_closedBall`, `ae_tendsto_limRatio`, `eventually_filterAt_mem_setsAt`, `ae_tendsto_average_norm_sub`, `ae_tendsto_div`, `ae_tendsto_measure_inter_div`, `ae_eventually_measure_zero_of_singular`, `mem_filterAt_iff`, `ae_tendsto_lintegral_div'`, `eventually_filterAt_subset_of_nhds`, `eventually_filterAt_measurableSet`, `eventually_filterAt_integrableOn`, `tendsto_filterAt_iff`, `filterAt_neBot`, `ae_tendsto_rnDeriv_of_absolutelyContinuous`, `frequently_filterAt_iff`, `ae_tendsto_rnDeriv`, `Real.tendsto_Icc_vitaliFamily_left`, `Besicovitch.tendsto_filterAt`, `fineSubfamilyOn_iff_frequently`, `ae_eventually_measure_pos`, `filterAt_enlarge`, `IsUnifLocDoublingMeasure.tendsto_closedBall_filterAt`, `ae_tendsto_limRatioMeas`, `eventually_measure_lt_top`, `ae_tendsto_average`, `eventually_filterAt_subset_closedBall`, `ae_tendsto_lintegral_enorm_sub_div_of_integrable`, `ae_tendsto_lintegral_enorm_sub_div`, `ae_tendsto_lintegral_enorm_sub_div'_of_integrable`, `Real.tendsto_Icc_vitaliFamily_right`
`mono` 📖	CompOp	—
`setsAt` 📖	CompOp	11 math math: `Real.Icc_mem_vitaliFamily_at_left`, `Filter.HasBasis.vitaliFamily`, `filterAt_basis_closedBall`, `eventually_filterAt_mem_setsAt`, `IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul`, `FineSubfamilyOn.covering_mem_family`, `FineSubfamilyOn.exists_disjoint_covering_ae`, `tendsto_filterAt_iff`, `frequently_filterAt_iff`, `nontrivial`, `Real.Icc_mem_vitaliFamily_at_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`covering` 📖	mathematical	`Set` `Set.instHasSubset` `setsAt` `Set.instMembership` `Metric.closedBall`	`Set.PairwiseDisjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instSDiff` `Set.iUnion` `instZeroENNReal`	—	—
`eventually_filterAt_iff` 📖	mathematical	—	`Filter.Eventually` `Set` `filterAt` `Real` `Real.instLT` `Real.instZero`	—	`mem_filterAt_iff`
`eventually_filterAt_measurableSet` 📖	mathematical	—	`Filter.Eventually` `Set` `MeasurableSet` `filterAt`	—	`Filter.mp_mem` `eventually_filterAt_mem_setsAt` `Filter.univ_mem'` `measurableSet`
`eventually_filterAt_mem_setsAt` 📖	mathematical	—	`Filter.Eventually` `Set` `Set.instMembership` `setsAt` `filterAt`	—	`tendsto_filterAt_iff` `Filter.tendsto_id`
`eventually_filterAt_subset_closedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Eventually` `Set` `Set.instHasSubset` `Metric.closedBall` `filterAt`	—	`tendsto_filterAt_iff` `Filter.tendsto_id`
`eventually_filterAt_subset_of_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`Filter.Eventually` `Set.instHasSubset` `filterAt`	—	`Filter.Eventually.filter_mono` `inf_le_left` `Filter.eventually_smallSets_subset`
`filterAt_basis_closedBall` 📖	mathematical	—	`Filter.HasBasis` `Set` `Real` `filterAt` `Real.instLT` `Real.instZero` `setOf` `Set.instMembership` `setsAt` `Set.instHasSubset` `Metric.closedBall`	—	`Filter.HasBasis.vitaliFamily` `Metric.nhds_basis_closedBall`
`filterAt_enlarge` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`filterAt` `enlarge`	—	`Filter.mp_mem` `Filter.eventually_smallSets_subset` `Metric.closedBall_mem_nhds` `Filter.univ_mem'` `instIsEmptyFalse` `inf_sup_left`
`filterAt_neBot` 📖	mathematical	—	`Filter.NeBot` `Set` `filterAt`	—	`Filter.HasBasis.neBot_iff` `filterAt_basis_closedBall` `nontrivial`
`fineSubfamilyOn_iff_frequently` 📖	mathematical	—	`FineSubfamilyOn` `Filter.Frequently` `Set` `Set.instMembership` `filterAt`	—	—
`fineSubfamilyOn_of_frequently` 📖	mathematical	`Filter.Frequently` `Set` `Set.instMembership` `filterAt`	`FineSubfamilyOn`	—	`fineSubfamilyOn_iff_frequently`
`frequently_filterAt_iff` 📖	mathematical	—	`Filter.Frequently` `Set` `filterAt` `Set.instMembership` `setsAt` `Set.instHasSubset` `Metric.closedBall`	—	`Filter.HasBasis.frequently_iff` `filterAt_basis_closedBall`
`measurableSet` 📖	mathematical	`Set` `Set.instMembership` `setsAt`	`MeasurableSet`	—	—
`mem_filterAt_iff` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `filterAt` `Real` `Real.instLT` `Real.instZero` `Set.instMembership`	—	`Filter.HasBasis.mem_iff` `filterAt_basis_closedBall`
`nonempty_interior` 📖	mathematical	`Set` `Set.instMembership` `setsAt`	`Set.Nonempty` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	—
`nontrivial` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.instMembership` `setsAt` `Set.instHasSubset` `Metric.closedBall`	—	—
`tendsto_filterAt_iff` 📖	mathematical	—	`Filter.Tendsto` `Set` `filterAt` `Filter.Eventually` `Set.instMembership` `setsAt` `Set.instHasSubset` `Metric.closedBall`	—	`Filter.HasBasis.tendsto_right_iff` `Filter.HasBasis.smallSets` `Metric.nhds_basis_closedBall`

VitaliFamily.FineSubfamilyOn

Definitions

Name	Category	Theorems
`covering` 📖	CompOp	8 math math: `measure_diff_biUnion`, `measure_le_tsum`, `covering_mem`, `covering_mem_family`, `covering_disjoint_subtype`, `measurableSet_u`, `measure_le_tsum_of_absolutelyContinuous`, `covering_disjoint`
`index` 📖	CompOp	6 math math: `measure_diff_biUnion`, `measure_le_tsum`, `covering_disjoint_subtype`, `index_countable`, `measure_le_tsum_of_absolutelyContinuous`, `covering_disjoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`covering_disjoint` 📖	mathematical	`VitaliFamily.FineSubfamilyOn`	`Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `index` `covering`	—	`exists_disjoint_covering_ae`
`covering_disjoint_subtype` 📖	mathematical	`VitaliFamily.FineSubfamilyOn`	`Pairwise` `Set.Elem` `Set` `index` `Function.onFun` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `covering` `Set.instMembership`	—	`pairwise_subtype_iff_pairwise_set` `covering_disjoint`
`covering_mem` 📖	mathematical	`VitaliFamily.FineSubfamilyOn` `Set` `Set.instMembership` `index`	`covering`	—	`exists_disjoint_covering_ae`
`covering_mem_family` 📖	mathematical	`VitaliFamily.FineSubfamilyOn` `Set` `Set.instMembership` `index`	`VitaliFamily.setsAt` `covering`	—	`exists_disjoint_covering_ae`
`exists_disjoint_covering_ae` 📖	mathematical	`VitaliFamily.FineSubfamilyOn`	`Set` `Set.instMembership` `Set.PairwiseDisjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instInter` `VitaliFamily.setsAt` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instSDiff` `Set.iUnion` `instZeroENNReal`	—	`VitaliFamily.covering` `Set.inter_subset_left`
`index_countable` 📖	mathematical	`VitaliFamily.FineSubfamilyOn`	`Set.Countable` `Set` `index`	—	`Set.PairwiseDisjoint.countable_of_nonempty_interior` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `covering_disjoint` `VitaliFamily.nonempty_interior` `covering_mem_family`
`index_subset` 📖	—	`VitaliFamily.FineSubfamilyOn` `Set` `Set.instMembership` `index`	—	—	`exists_disjoint_covering_ae`
`measurableSet_u` 📖	mathematical	`VitaliFamily.FineSubfamilyOn` `Set` `Set.instMembership` `index`	`MeasurableSet` `covering`	—	`VitaliFamily.measurableSet` `covering_mem_family`
`measure_diff_biUnion` 📖	mathematical	`VitaliFamily.FineSubfamilyOn`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instSDiff` `Set.iUnion` `Set.instMembership` `index` `covering` `instZeroENNReal`	—	`exists_disjoint_covering_ae`
`measure_le_tsum` 📖	mathematical	`VitaliFamily.FineSubfamilyOn`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `tsum` `Set.Elem` `index` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `covering` `Set.instMembership` `SummationFilter.unconditional`	—	`measure_le_tsum_of_absolutelyContinuous` `MeasureTheory.Measure.AbsolutelyContinuous.rfl`
`measure_le_tsum_of_absolutelyContinuous` 📖	mathematical	`VitaliFamily.FineSubfamilyOn` `MeasureTheory.Measure.AbsolutelyContinuous`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `tsum` `Set.Elem` `index` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `covering` `Set.instMembership` `SummationFilter.unconditional`	—	`MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.diff_union_self` `MeasureTheory.measure_union_le` `measure_diff_biUnion` `zero_add` `MeasureTheory.measure_biUnion` `index_countable` `covering_disjoint` `measurableSet_u`

(root)

Definitions

Name	Category	Theorems
`VitaliFamily` 📖	CompData	—

---

← Back to Index