OneDim

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

Statistics

Metric	Count
Definitions	0
Theorems Icc_mem_vitaliFamily_at_left, Icc_mem_vitaliFamily_at_right, tendsto_Icc_vitaliFamily_left, tendsto_Icc_vitaliFamily_right	4
Total	4

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_mem_vitaliFamily_at_left 📖	mathematical	Real instLT	Set Set.instMembership VitaliFamily.setsAt pseudoMetricSpace MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal borelSpace FiniteDimensional.rclike_to_real instIsAddHaarMeasureVolume measurableSpace instSecondCountableTopologyReal locallyFinite_volume instOne Set.Icc instPreorder	—	MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure borelSpace FiniteDimensional.rclike_to_real instIsAddHaarMeasureVolume instSecondCountableTopologyReal locallyFinite_volume Nat.instAtLeastTwoHAddOfNat Icc_eq_closedBall IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul dist_eq abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid le_of_not_gt 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.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 Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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 Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing CancelDenoms.sub_subst CancelDenoms.div_subst CancelDenoms.add_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 RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true CancelDenoms.mul_subst lt_of_not_ge Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le
Icc_mem_vitaliFamily_at_right 📖	mathematical	Real instLT	Set Set.instMembership VitaliFamily.setsAt pseudoMetricSpace MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal borelSpace FiniteDimensional.rclike_to_real instIsAddHaarMeasureVolume measurableSpace instSecondCountableTopologyReal locallyFinite_volume instOne Set.Icc instPreorder	—	MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure borelSpace FiniteDimensional.rclike_to_real instIsAddHaarMeasureVolume instSecondCountableTopologyReal locallyFinite_volume Nat.instAtLeastTwoHAddOfNat Icc_eq_closedBall IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul dist_comm dist_eq abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid le_of_not_gt 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.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 Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Linarith.add_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing CancelDenoms.sub_subst CancelDenoms.div_subst CancelDenoms.add_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 RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq CancelDenoms.mul_subst lt_of_not_ge Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le
tendsto_Icc_vitaliFamily_left 📖	mathematical	—	Filter.Tendsto Real Set Set.Icc instPreorder nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Set.Iio VitaliFamily.filterAt MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal borelSpace FiniteDimensional.rclike_to_real instIsAddHaarMeasureVolume measurableSpace instSecondCountableTopologyReal locallyFinite_volume instOne	—	MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure borelSpace FiniteDimensional.rclike_to_real instIsAddHaarMeasureVolume instSecondCountableTopologyReal locallyFinite_volume VitaliFamily.tendsto_filterAt_iff Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' Icc_mem_vitaliFamily_at_left Icc_mem_nhdsLT instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero 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_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le closedBall_eq_Icc Set.Icc_subset_Icc le_of_not_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Linarith.add_neg
tendsto_Icc_vitaliFamily_right 📖	mathematical	—	Filter.Tendsto Real Set Set.Icc instPreorder nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Set.Ioi VitaliFamily.filterAt MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal borelSpace FiniteDimensional.rclike_to_real instIsAddHaarMeasureVolume measurableSpace instSecondCountableTopologyReal locallyFinite_volume instOne	—	MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure borelSpace FiniteDimensional.rclike_to_real instIsAddHaarMeasureVolume instSecondCountableTopologyReal locallyFinite_volume VitaliFamily.tendsto_filterAt_iff Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' Icc_mem_vitaliFamily_at_right Icc_mem_nhdsGT instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero 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_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt 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.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le closedBall_eq_Icc Set.Icc_subset_Icc le_of_not_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_neg

---

← Back to Index