Vitali

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

Statistics

Metric	Count
Definitions vitaliFamily	1
Theorems exists_disjoint_covering_ae, exists_disjoint_covering_ae', exists_disjoint_subfamily_covering_enlargement, exists_disjoint_subfamily_covering_enlargement_closedBall	4
Total	5

Vitali

Definitions

Name	Category	Theorems
vitaliFamily 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_disjoint_covering_ae 📖	mathematical	Set Set.instHasSubset Metric.closedBall ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure MeasureTheory.Measure.instFunLike Real Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal Set.Nonempty interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace IsClosed Set.instMembership Real.instLE	Set.Countable Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instSDiff Set.iUnion instZeroENNReal	—	Nat.instAtLeastTwoHAddOfNat Filter.Eventually.exists_gt nhdsGT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.Eventually.and eventually_le_nhds instClosedIciTopology OrderTopology.to_orderClosedTopology one_pos Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Filter.Tendsto.comp tendsto_closedBall_smallSets Continuous.tendsto' Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.fst continuous_id' Continuous.snd Continuous.prodMk continuous_const MulZeroClass.mul_zero MeasureTheory.Measure.FiniteAtFilter.eventually MeasureTheory.Measure.finiteAt_nhds LE.le.trans Set.Nonempty.mono interior_subset exists_disjoint_subfamily_covering_enlargement one_lt_two IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Metric.nonempty_closedBall Set.PairwiseDisjoint.countable_of_nonempty_interior TopologicalSpace.SecondCountableTopology.to_separableSpace MeasureTheory.measure_null_of_locally_null MeasureTheory.Measure.instOuterMeasureClass Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall Set.inter_subset_inter Metric.ball_subset_closedBall Set.mem_image le_trans le_total HasSubset.Subset.trans Set.instIsTransSubset Metric.closedBall_subset_closedBall' le_csSup Set.mem_image_of_mem le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.add_nonpos Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.mul_neg LT.lt.trans_le lt_irrefl le_of_eq Real.sSup_empty Set.image_empty Set.nonempty_iff_ne_empty exists_lt_of_lt_csSup Set.Nonempty.image half_lt_self lt_of_le_of_lt MeasureTheory.measure_mono dist_comm Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Meta.NormNum.isNat_mul CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos inter_mem_nhdsWithin Metric.ball_mem_nhds nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd le_of_forall_gt_imp_ge_of_dense ENNReal.instDenselyOrdered MeasureTheory.measure_biUnion Set.Countable.mono Set.PairwiseDisjoint.subset IsClosed.measurableSet Set.iUnion₂_subset Filter.Eventually.exists Filter.atTop_neBot Finset.isDirected_le tendsto_order ENNReal.instOrderTopology ENNReal.tendsto_tsum_compl_atTop_zero LT.lt.ne LT.lt.ne' isClosed_biUnion_finset Set.mem_inter Set.mem_of_mem_inter_left Set.mem_biUnion Set.diff_inter_self IsOpen.mem_nhds IsOpen.sdiff Metric.isOpen_ball Set.mem_diff Set.mem_of_mem_inter_right Filter.HasBasis.mem_iff Metric.nhds_basis_closedBall lt_min Set.Subset.trans Metric.closedBall_subset_closedBall min_le_left Set.diff_subset min_le_right Set.inter_comm Set.inter_subset_inter_right Finset.subset_set_biUnion_of_mem Metric.mem_closedBall' Metric.mem_closedBall dist_triangle Set.subset_iUnion MeasureTheory.measure_iUnion_le Subtype.countable Set.Countable.to_subtype ENNReal.tsum_le_tsum ENNReal.tsum_mul_left mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid le_of_lt ENNReal.mul_div_le
exists_disjoint_covering_ae' 📖	mathematical	Set Set.instHasSubset Metric.closedBall ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure MeasureTheory.Measure.instFunLike Real Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal Set.Nonempty interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace IsClosed Filter.Frequently Set.instMembership nhdsWithin Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder	Set.Countable Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instSDiff Set.iUnion instZeroENNReal	—	Nat.instAtLeastTwoHAddOfNat frequently_nhds_iff frequently_nhdsWithin_iff isOpen_Ioo OrderTopology.to_orderClosedTopology instOrderTopologyReal exists_disjoint_covering_ae
exists_disjoint_subfamily_covering_enlargement 📖	mathematical	Real Real.instLT Real.instOne Real.instLE Real.instZero Set.Nonempty	Set Set.instHasSubset Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instMembership Set.instInter Real.instMul	—	zorn_subset Set.pairwiseDisjoint_sUnion IsChain.directedOn Set.instReflSubset Set.subset_sUnion_of_mem Maximal.prop Set.not_disjoint_iff_nonempty_inter lt_irrefl LT.lt.trans_le Mathlib.Tactic.Push.not_and_eq Set.mem_image LE.le.trans le_csSup Set.mem_image_of_mem eq_or_lt_of_le zero_div div_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero mul_one mul_lt_mul_of_pos_left IsStrictOrderedRing.toPosMulStrictMono exists_lt_of_lt_csSup Set.Nonempty.image LT.lt.le Set.Nonempty.ne_empty disjoint_self Maximal.mem_of_prop_insert Set.insert_subset_iff Set.PairwiseDisjoint.insert Set.mem_insert_of_mem Set.mem_insert_iff Set.mem_insert Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono le_of_lt
exists_disjoint_subfamily_covering_enlargement_closedBall 📖	mathematical	Real Real.instLE Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Set Set.instHasSubset Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Metric.closedBall Set.instMembership Real.instMul	—	Nat.instAtLeastTwoHAddOfNat Set.eq_empty_or_nonempty Set.Subset.refl Set.pairwiseDisjoint_empty Set.Subset.rfl Metric.closedBall_eq_empty exists_disjoint_subfamily_covering_enlargement lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true Metric.mem_closedBall_self Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall Metric.closedBall_subset_closedBall' le_of_not_gt Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.add_nonpos CancelDenoms.mul_subst HasSubset.Subset.trans Set.instIsTransSubset le_or_gt Mathlib.Tactic.Push.not_forall_eq

---

← Back to Index