GeometryOfNumbers

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

Statistics

Metric	Count
Definitions	0
Theorems exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure, exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure, exists_pair_mem_lattice_not_disjoint_vadd	3
Total	3

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure 📖	—	IsAddFundamentalDomain AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zero AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup.normedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddAction.instAddAction AddTorsor.toAddAction NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor Set Set.instMembership NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField IsCompact ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Measure.instFunLike Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Module.finrank	—	—	Nat.instAtLeastTwoHAddOfNat IsAddFundamentalDomain.measure_ne_zero Subgroup.vaddInvariantMeasure Measure.IsAddLeftInvariant.vaddInvariantMeasure Measure.IsAddHaarMeasure.toIsAddLeftInvariant Measure.instNeZeroOfNonempty Measure.IsAddHaarMeasure.toIsOpenPosMeasure Nontrivial.to_nonempty ENNReal.instCanonicallyOrderedAdd ENNReal.instNoZeroDivisors isReduced_of_noZeroDivisors ENNReal.instCharZero nonempty_of_measure_ne_zero exists_seq_strictAnti_tendsto NNReal.instOrderTopology NNReal.instDenselyOrdered IsStrictOrderedRing.toNoMaxOrder NNReal.instIsStrictOrderedRing TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ConvexBody.zero_mem_of_symmetric isOpen_inter_eq_singleton_of_mem_discrete ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass AddSubgroup.instAddSubgroupClass sdiff_eq_sdiff_iff_inf_eq_inf inf_of_le_right Set.inter_comm IsClosed.sdiff AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed Set.inter_subset_inter_left SetLike.coe_subset_coe instIsConcreteLE ConvexBody.smul_le_of_le add_le_add_iff_left NNReal.addLeftMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd NNReal.addLeftReflectLT le_of_lt lt_of_le_of_lt ConvexBody.coe_smul' NNReal.smul_def Measure.addHaar_smul_of_nonneg NNReal.coe_nonneg one_mul ENNReal.mul_lt_mul_left ne_of_gt lt_of_le_of_ne' zero_le IsCompact.measure_ne_top Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts ENNReal.ofReal_pow add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one one_lt_pow₀ IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing IsOrderedRing.toPosMulMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono contravariant_lt_of_covariant_le Module.finrank_pos commRing_strongRankCondition Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors smul_neg exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure ConvexBody.convex IsCompact.inter_right ConvexBody.isCompact IsClosed.inter ConvexBody.isClosed ConvexBody.iInter_smul_eq_self Set.iInter_inter
exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure 📖	—	IsAddFundamentalDomain AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zero AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup.normedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddAction.instAddAction AddTorsor.toAddAction NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor Set Set.instMembership NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Measure.instFunLike Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Module.finrank	—	—	Nat.instAtLeastTwoHAddOfNat Measure.addHaar_smul_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing ENNReal.mul_lt_mul_iff_left pow_ne_zero isReduced_of_noZeroDivisors ENNReal.instNoZeroDivisors two_ne_zero' CharZero.NeZero.two ENNReal.instCharZero ENNReal.pow_ne_top ENNReal.ofNat_ne_top mul_right_comm ENNReal.ofReal_pow ENNReal.ofReal_inv_of_pos zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ENNReal.ofReal_ofNat mul_pow ENNReal.inv_mul_cancel two_ne_zero one_pow one_mul exists_pair_mem_lattice_not_disjoint_vadd AddSubgroup.instMeasurableVAdd measurableVAdd_of_add ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Subgroup.vaddInvariantMeasure Measure.IsAddLeftInvariant.vaddInvariantMeasure Measure.IsAddHaarMeasure.toIsAddLeftInvariant Convex.nullMeasurableSet Convex.smul Set.not_disjoint_iff sub_ne_zero add_comm inv_smul_smul₀ smul_sub sub_eq_add_neg smul_add Set.mem_inv_smul_set_iff₀ Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Nat.cast_one
exists_pair_mem_lattice_not_disjoint_vadd 📖	mathematical	IsAddFundamentalDomain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NullMeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike	Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice HVAdd.hVAdd instHVAdd Set.vaddSet	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq Eq.trans_le IsAddFundamentalDomain.measure_eq_tsum MeasurableVAdd.toMeasurableConstVAdd measure_iUnion₀ Pairwise.mono Disjoint.aedisjoint Disjoint.mono inf_le_left NullMeasurableSet.inter NullMeasurableSet.vadd IsAddFundamentalDomain.nullMeasurableSet measure_mono Measure.instOuterMeasureClass Set.iUnion_subset Set.inter_subset_right

---

← Back to Index