AddCircle

📁 Source: Mathlib/MeasureTheory/Group/AddCircle.lean

Statistics

Metric	Count
Definitions	0
Theorems closedBall_ae_eq_ball, isAddFundamentalDomain_of_ae_ball, volume_of_add_preimage_eq	3
Total	3

AddCircle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedBall_ae_eq_ball 📖	mathematical	—	Filter.EventuallyEq AddCircle Real Real.instAddCommGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace QuotientAddGroup.instSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing AddSubgroup.zmultiples AddCommGroup.toAddGroup Metric.ball	—	MeasureTheory.Measure.instOuterMeasureClass le_or_gt Metric.ball_eq_empty MeasureTheory.ae_eq_empty Nat.instAtLeastTwoHAddOfNat volume_closedBall min_eq_right 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.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero 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.zero_mul 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.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_zero_add Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.mul_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_neg_of_lt Fact.out ENNReal.ofReal_eq_zero mul_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono zero_le_two Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ENNReal.tendsto_ofReal Filter.Tendsto.min HasSolidNorm.orderClosedTopology instHasSolidNormReal tendsto_const_nhds Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal nhdsWithin_le_nhds le_of_tendsto instClosedIicTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology nhdsLT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instNontrivial Filter.mem_of_superset Ioo_mem_nhdsLT MeasureTheory.measure_mono Metric.closedBall_subset_ball Filter.EventuallyEq.symm MeasureTheory.ae_eq_of_subset_of_measure_ge Metric.ball_subset_closedBall MeasurableSet.nullMeasurableSet measurableSet_ball BorelSpace.opensMeasurable QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples MeasureTheory.measure_ne_top isFiniteMeasure
isAddFundamentalDomain_of_ae_ball 📖	mathematical	IsOfFinAddOrder AddCircle Real Real.instAddCommGroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroupReal ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume Metric.ball QuotientAddGroup.instSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing AddSubgroup.zmultiples AddCommGroup.toAddGroup DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat addOrderOf	MeasureTheory.IsAddFundamentalDomain AddSubgroup QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zero AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddSubgroup.normedAddCommGroup AddAction.toAddSemigroupAction AddAction.instAddAction AddTorsor.toAddAction NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor QuotientAddGroup.measurableSpace Real.measurableSpace	—	MeasureTheory.Measure.instOuterMeasureClass Nat.instAtLeastTwoHAddOfNat AddSubgroup.normal_of_comm Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add 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.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Nat.cast_zero IsOfFinAddOrder.addOrderOf_pos MeasureTheory.IsAddFundamentalDomain.mk_of_measure_univ_le isFiniteMeasure AddSubgroup.instCountableSubtypeMemZMultiples MeasureTheory.NullMeasurableSet.congr MeasurableSet.nullMeasurableSet measurableSet_ball BorelSpace.opensMeasurable QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples Filter.EventuallyEq.symm MeasureTheory.AEDisjoint.congr Disjoint.aedisjoint add_comm singleton_add_ball add_ball Metric.thickening_singleton Metric.ball_disjoint_ball dist_eq_norm add_sub_cancel_right div_mul_eq_div_div add_div add_self_div_two CharZero.NeZero.two div_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial nsmul_eq_mul LE.le.trans le_add_order_smul_norm_of_isOfFinAddOrder IsOfFinAddOrder.of_mem_zmultiples nsmul_le_nsmul_left norm_nonneg addOrderOf_pos_iff addOrderOf_dvd_of_mem_zmultiples MeasureTheory.Measure.QuasiMeasurePreserving.vadd_ae_eq_of_ae_eq MeasureTheory.quasiMeasurePreserving_add_left ContinuousAdd.measurableMul₂ QuotientAddGroup.instSecondCountableTopology IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalAddGroup.toContinuousAdd QuotientAddGroup.instIsTopologicalAddGroup MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureRealVolume CompactSpace.sigmaCompact compactSpace ContinuousNeg.measurableNeg IsTopologicalAddGroup.toContinuousNeg MeasureTheory.IsAddLeftInvariant.isAddRightInvariant MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant Filter.EventuallyEq.trans closedBall_ae_eq_ball Set.Finite.to_subtype IsOfFinAddOrder.finite_zmultiples Nat.card_zmultiples Nat.card_eq_fintype_card MeasureTheory.measure_vadd MeasureTheory.Subgroup.vaddInvariantMeasure MeasureTheory.Measure.IsAddLeftInvariant.vaddInvariantMeasure measure_univ tsum_fintype SummationFilter.instLeAtTopUnconditional Finset.sum_const MeasureTheory.measure_congr volume_closedBall ENNReal.ofReal_nsmul mul_div mul_div_mul_comm div_self two_ne_zero one_mul min_eq_right div_le_self LT.lt.le Fact.out mul_div_cancel₀ LT.lt.ne zero_lt_one NeZero.charZero_one le_refl
volume_of_add_preimage_eq 📖	mathematical	IsOfFinAddOrder AddCircle Real Real.instAddCommGroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroupReal ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction AddTorsor.toAddAction QuotientAddGroup.Quotient.addGroup AddCommGroup.toAddGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm NormedAddTorsor.toAddTorsor QuotientAddGroup.instSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddCommGroup.toNormedAddTorsor Metric.ball DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat addOrderOf	DFunLike.coe ENNReal AddMonoid.toNatSMul ENNReal.instTopologicalSpace instENormedAddCommMonoidENNReal Set.instInter	—	MeasureTheory.Measure.instOuterMeasureClass AddSubgroup.normal_of_comm Nat.instAtLeastTwoHAddOfNat MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples MeasureTheory.Measure.IsAddLeftInvariant.vaddInvariantMeasure MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant instIsAddHaarMeasureRealVolume MeasureTheory.IsAddFundamentalDomain.measure_eq_card_smul_of_vadd_ae_eq_self AddSubgroup.instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_of_add ContinuousAdd.measurableAdd QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples IsTopologicalAddGroup.toContinuousAdd QuotientAddGroup.instIsTopologicalAddGroup MeasureTheory.Subgroup.vaddInvariantMeasure AddSubgroup.instCountableSubtypeMemZMultiples Finite.of_fintype Set.Finite.to_subtype IsOfFinAddOrder.finite_zmultiples isAddFundamentalDomain_of_ae_ball Nat.card_zmultiples

---

← Back to Index