Basic

📁 Source: Mathlib/MeasureTheory/Measure/Haar/Basic.lean

Statistics

Metric	Count
Definitions addHaar, addHaarMeasure, haar, addCHaar, addHaarContent, addHaarProduct, addIndex, addPrehaar, chaar, clAddPrehaar, clPrehaar, haarContent, haarProduct, index, prehaar, haarMeasure	16
Theorems addHaarMeasure_apply, addHaarMeasure_closure_self, addHaarMeasure_eq_iff, addHaarMeasure_self, addHaarMeasure_unique, div_mem_nhds_one_of_haar_pos, div_mem_nhds_one_of_haar_pos_ne_top, addCHaar_empty, addCHaar_mem_addHaarProduct, addCHaar_mem_clAddPrehaar, addCHaar_mono, addCHaar_nonneg, addCHaar_self, addCHaar_sup_eq, addCHaar_sup_le, addHaarContent_apply, addHaarContent_outerMeasure_closure_pos, addHaarContent_outerMeasure_self_pos, addHaarContent_self, addIndex_defined, addIndex_elim, addIndex_empty, addIndex_mono, addIndex_pos, addIndex_union_eq, addIndex_union_le, addPrehaar_empty, addPrehaar_mem_addHaarProduct, addPrehaar_mono, addPrehaar_nonneg, addPrehaar_pos, addPrehaar_self, addPrehaar_sup_eq, addPrehaar_sup_le, add_left_addIndex_le, add_prehaar_le_addIndex, chaar_empty, chaar_mem_clPrehaar, chaar_mem_haarProduct, chaar_mono, chaar_nonneg, chaar_self, chaar_sup_eq, chaar_sup_le, haarContent_apply, haarContent_outerMeasure_closure_pos, haarContent_outerMeasure_self_pos, haarContent_self, index_defined, index_elim, index_empty, index_mono, index_pos, index_union_eq, index_union_le, is_left_invariant_addCHaar, is_left_invariant_addHaarContent, is_left_invariant_addIndex, is_left_invariant_addPrehaar, is_left_invariant_chaar, is_left_invariant_haarContent, is_left_invariant_index, is_left_invariant_prehaar, le_addIndex_mul, le_index_mul, mem_addPrehaar_empty, mem_prehaar_empty, mul_left_index_le, nonempty_iInter_clAddPrehaar, nonempty_iInter_clPrehaar, prehaar_empty, prehaar_le_index, prehaar_mem_haarProduct, prehaar_mono, prehaar_nonneg, prehaar_pos, prehaar_self, prehaar_sup_eq, prehaar_sup_le, haarMeasure_apply, haarMeasure_closure_self, haarMeasure_eq_iff, haarMeasure_self, haarMeasure_unique, isAddHaarMeasure_addHaarMeasure, isAddLeftInvariant_addHaarMeasure, isHaarMeasure_haarMeasure, isMulLeftInvariant_haarMeasure, regular_addHaarMeasure, regular_haarMeasure, regular_of_isAddLeftInvariant, regular_of_isMulLeftInvariant, sigmaFinite_addHaarMeasure, sigmaFinite_haarMeasure, sub_mem_nhds_zero_of_addHaar_pos, sub_mem_nhds_zero_of_addHaar_pos_ne_top	96
Total	112

MeasureTheory.Measure

Definitions

Name	Category	Theorems
addHaar 📖	CompOp	5 math math: MeasureTheory.distribHaarChar_apply, ExistsContDiffBumpBase.u_int_pos, ExistsContDiffBumpBase.w_def, ExistsContDiffBumpBase.w_integral, LinearMap.exists_map_addHaar_eq_smul_addHaar'
addHaarMeasure 📖	CompOp	13 math math: isAddLeftInvariant_addHaarMeasure, addHaarMeasure_closure_self, regular_addHaarMeasure, addHaarMeasure_eq_iff, addHaarMeasure_unique, sigmaFinite_addHaarMeasure, addHaarMeasure_apply, Module.Basis.addHaar_def, addHaarMeasure_self, MeasureTheory.addHaarMeasure_eq_volume_pi, isAddHaarMeasure_addHaarMeasure, MeasureTheory.addHaarMeasure_eq_volume, IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure
haar 📖	CompOp	—
haarMeasure 📖	CompOp	10 math math: haarMeasure_closure_self, haarMeasure_apply, haarMeasure_unique, isMulLeftInvariant_haarMeasure, haarMeasure_self, isHaarMeasure_haarMeasure, IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure, regular_haarMeasure, sigmaFinite_haarMeasure, haarMeasure_eq_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addHaarMeasure_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike addHaarMeasure DivInvMonoid.toDiv ENNReal.instDivInvMonoid MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.Content.outerMeasure haar.addHaarContent MeasureTheory.Content.measure instR1Space IsTopologicalAddGroup.regularSpace SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	instR1Space IsTopologicalAddGroup.regularSpace MeasureTheory.Content.measure_apply mul_comm div_eq_mul_inv
addHaarMeasure_closure_self 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike addHaarMeasure closure SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsCompact.measure_closure instR1Space IsTopologicalAddGroup.regularSpace TopologicalSpace.PositiveCompacts.isCompact addHaarMeasure_self
addHaarMeasure_eq_iff 📖	mathematical	—	addHaarMeasure DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	addHaarMeasure_self IsScalarTower.right addHaarMeasure_unique one_smul
addHaarMeasure_self 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike addHaarMeasure SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsCompact.measure_closure instR1Space IsTopologicalAddGroup.regularSpace TopologicalSpace.PositiveCompacts.isCompact MeasureTheory.Content.measure_apply IsClosed.measurableSet BorelSpace.opensMeasurable isClosed_closure ENNReal.inv_mul_cancel LT.lt.ne' haar.addHaarContent_outerMeasure_closure_pos LT.lt.ne MeasureTheory.Content.outerMeasure_lt_top_of_isCompact instWeaklyLocallyCompactSpaceOfLocallyCompactSpace TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup IsCompact.closure
addHaarMeasure_unique 📖	mathematical	—	ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set instFunLike SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike addHaarMeasure	—	Set.Nonempty.mono interior_mono subset_closure TopologicalSpace.PositiveCompacts.interior_nonempty IsScalarTower.right MeasureTheory.measure_eq_sub_vadd ContinuousAdd.measurableMul₂ IsTopologicalAddGroup.toContinuousAdd ContinuousNeg.measurableNeg IsTopologicalAddGroup.toContinuousNeg sigmaFinite_addHaarMeasure isAddLeftInvariant_addHaarMeasure LT.lt.ne' measure_pos_of_nonempty_interior IsAddHaarMeasure.toIsOpenPosMeasure isAddHaarMeasure_addHaarMeasure IsCompact.measure_ne_top IsAddHaarMeasure.toIsFiniteMeasureOnCompacts IsCompact.closure instR1Space IsTopologicalAddGroup.regularSpace TopologicalSpace.PositiveCompacts.isCompact IsCompact.measure_closure div_one addHaarMeasure_closure_self
div_mem_nhds_one_of_haar_pos 📖	mathematical	MeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure Set instFunLike	Filter Filter.instMembership nhds InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set.div DivInvMonoid.toDiv Group.toDivInvMonoid	—	InnerRegular.instInnerRegularCompactLTTop MeasurableSet.exists_lt_isCompact
div_mem_nhds_one_of_haar_pos_ne_top 📖	mathematical	MeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure Set instFunLike	Filter Filter.instMembership nhds InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set.div DivInvMonoid.toDiv Group.toDivInvMonoid	—	MeasurableSet.exists_lt_isCompact_of_ne_top
haarMeasure_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike haarMeasure DivInvMonoid.toDiv ENNReal.instDivInvMonoid MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.Content.outerMeasure haar.haarContent MeasureTheory.Content.measure instR1Space IsTopologicalGroup.regularSpace SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	instR1Space IsTopologicalGroup.regularSpace MeasureTheory.Content.measure_apply mul_comm div_eq_mul_inv
haarMeasure_closure_self 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike haarMeasure closure SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsCompact.measure_closure instR1Space IsTopologicalGroup.regularSpace TopologicalSpace.PositiveCompacts.isCompact haarMeasure_self
haarMeasure_eq_iff 📖	mathematical	—	haarMeasure DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	haarMeasure_self IsScalarTower.right haarMeasure_unique one_smul
haarMeasure_self 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike haarMeasure SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsCompact.measure_closure instR1Space IsTopologicalGroup.regularSpace TopologicalSpace.PositiveCompacts.isCompact MeasureTheory.Content.measure_apply IsClosed.measurableSet BorelSpace.opensMeasurable isClosed_closure ENNReal.inv_mul_cancel LT.lt.ne' haar.haarContent_outerMeasure_closure_pos LT.lt.ne MeasureTheory.Content.outerMeasure_lt_top_of_isCompact instWeaklyLocallyCompactSpaceOfLocallyCompactSpace TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group IsCompact.closure
haarMeasure_unique 📖	mathematical	—	ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set instFunLike SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike haarMeasure	—	Set.Nonempty.mono interior_mono subset_closure TopologicalSpace.PositiveCompacts.interior_nonempty IsScalarTower.right MeasureTheory.measure_eq_div_smul ContinuousMul.measurableMul₂ IsTopologicalGroup.toContinuousMul ContinuousInv.measurableInv IsTopologicalGroup.toContinuousInv sigmaFinite_haarMeasure isMulLeftInvariant_haarMeasure LT.lt.ne' measure_pos_of_nonempty_interior IsHaarMeasure.toIsOpenPosMeasure isHaarMeasure_haarMeasure IsCompact.measure_ne_top IsHaarMeasure.toIsFiniteMeasureOnCompacts IsCompact.closure instR1Space IsTopologicalGroup.regularSpace TopologicalSpace.PositiveCompacts.isCompact IsCompact.measure_closure div_one haarMeasure_closure_self
isAddHaarMeasure_addHaarMeasure 📖	mathematical	—	IsAddHaarMeasure addHaarMeasure	—	isAddHaarMeasure_of_isCompact_nonempty_interior isAddLeftInvariant_addHaarMeasure TopologicalSpace.PositiveCompacts.isCompact TopologicalSpace.PositiveCompacts.interior_nonempty addHaarMeasure_self one_ne_zero NeZero.charZero_one ENNReal.instCharZero ENNReal.one_ne_top
isAddLeftInvariant_addHaarMeasure 📖	mathematical	—	IsAddLeftInvariant AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addHaarMeasure	—	MeasureTheory.forall_measure_preimage_add_iff ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd instR1Space IsTopologicalAddGroup.regularSpace addHaarMeasure_apply MeasurableAdd.measurable_const_add MeasureTheory.Content.is_add_left_invariant_outerMeasure haar.is_left_invariant_addHaarContent
isHaarMeasure_haarMeasure 📖	mathematical	—	IsHaarMeasure haarMeasure	—	isHaarMeasure_of_isCompact_nonempty_interior isMulLeftInvariant_haarMeasure TopologicalSpace.PositiveCompacts.isCompact TopologicalSpace.PositiveCompacts.interior_nonempty haarMeasure_self one_ne_zero NeZero.charZero_one ENNReal.instCharZero
isMulLeftInvariant_haarMeasure 📖	mathematical	—	IsMulLeftInvariant MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid haarMeasure	—	MeasureTheory.forall_measure_preimage_mul_iff ContinuousMul.measurableMul IsTopologicalGroup.toContinuousMul instR1Space IsTopologicalGroup.regularSpace haarMeasure_apply MeasurableMul.measurable_const_mul MeasureTheory.Content.is_mul_left_invariant_outerMeasure haar.is_left_invariant_haarContent
regular_addHaarMeasure 📖	mathematical	—	Regular addHaarMeasure	—	Regular.smul MeasureTheory.Content.regular instWeaklyLocallyCompactSpaceOfLocallyCompactSpace TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup IsCompact.measure_closure instR1Space IsTopologicalAddGroup.regularSpace TopologicalSpace.PositiveCompacts.isCompact MeasureTheory.Content.measure_apply IsClosed.measurableSet BorelSpace.opensMeasurable isClosed_closure ENNReal.inv_ne_top LT.lt.ne' haar.addHaarContent_outerMeasure_closure_pos
regular_haarMeasure 📖	mathematical	—	Regular haarMeasure	—	Regular.smul MeasureTheory.Content.regular instWeaklyLocallyCompactSpaceOfLocallyCompactSpace TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group IsCompact.measure_closure instR1Space IsTopologicalGroup.regularSpace TopologicalSpace.PositiveCompacts.isCompact MeasureTheory.Content.measure_apply IsClosed.measurableSet BorelSpace.opensMeasurable isClosed_closure ENNReal.inv_ne_top LT.lt.ne' haar.haarContent_outerMeasure_closure_pos
regular_of_isAddLeftInvariant 📖	mathematical	IsCompact Set.Nonempty interior	Regular	—	IsScalarTower.right addHaarMeasure_unique Regular.smul regular_addHaarMeasure
regular_of_isMulLeftInvariant 📖	mathematical	IsCompact Set.Nonempty interior	Regular	—	IsScalarTower.right haarMeasure_unique Regular.smul regular_haarMeasure
sigmaFinite_addHaarMeasure 📖	mathematical	—	MeasureTheory.SigmaFinite addHaarMeasure	—	MeasureTheory.sigmaFinite_of_locallyFinite MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts instWeaklyLocallyCompactSpaceOfLocallyCompactSpace TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup Regular.toIsFiniteMeasureOnCompacts regular_addHaarMeasure
sigmaFinite_haarMeasure 📖	mathematical	—	MeasureTheory.SigmaFinite haarMeasure	—	MeasureTheory.sigmaFinite_of_locallyFinite MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts instWeaklyLocallyCompactSpaceOfLocallyCompactSpace TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group Regular.toIsFiniteMeasureOnCompacts regular_haarMeasure
sub_mem_nhds_zero_of_addHaar_pos 📖	mathematical	MeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure Set instFunLike	Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Set.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	InnerRegular.instInnerRegularCompactLTTop MeasurableSet.exists_lt_isCompact
sub_mem_nhds_zero_of_addHaar_pos_ne_top 📖	mathematical	MeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure Set instFunLike	Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Set.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	MeasurableSet.exists_lt_isCompact_of_ne_top

MeasureTheory.Measure.haar

Definitions

Name	Category	Theorems
addCHaar 📖	CompOp	9 math math: addCHaar_mem_clAddPrehaar, addCHaar_nonneg, addCHaar_sup_le, is_left_invariant_addCHaar, addCHaar_mem_addHaarProduct, addCHaar_sup_eq, addCHaar_self, addCHaar_mono, addCHaar_empty
addHaarContent 📖	CompOp	6 math math: addHaarContent_apply, addHaarContent_outerMeasure_self_pos, addHaarContent_outerMeasure_closure_pos, addHaarContent_self, MeasureTheory.Measure.addHaarMeasure_apply, is_left_invariant_addHaarContent
addHaarProduct 📖	CompOp	4 math math: nonempty_iInter_clAddPrehaar, mem_addPrehaar_empty, addCHaar_mem_addHaarProduct, addPrehaar_mem_addHaarProduct
addIndex 📖	CompOp	11 math math: addIndex_union_eq, addIndex_empty, le_addIndex_mul, add_prehaar_le_addIndex, add_left_addIndex_le, mem_addPrehaar_empty, addIndex_union_le, addIndex_elim, addIndex_mono, addIndex_pos, is_left_invariant_addIndex
addPrehaar 📖	CompOp	10 math math: add_prehaar_le_addIndex, addPrehaar_sup_eq, addPrehaar_mono, addPrehaar_nonneg, addPrehaar_pos, is_left_invariant_addPrehaar, addPrehaar_mem_addHaarProduct, addPrehaar_sup_le, addPrehaar_self, addPrehaar_empty
chaar 📖	CompOp	9 math math: chaar_mono, chaar_nonneg, chaar_self, chaar_sup_eq, chaar_mem_haarProduct, chaar_sup_le, is_left_invariant_chaar, chaar_empty, chaar_mem_clPrehaar
clAddPrehaar 📖	CompOp	2 math math: nonempty_iInter_clAddPrehaar, addCHaar_mem_clAddPrehaar
clPrehaar 📖	CompOp	2 math math: nonempty_iInter_clPrehaar, chaar_mem_clPrehaar
haarContent 📖	CompOp	6 math math: MeasureTheory.Measure.haarMeasure_apply, haarContent_apply, haarContent_self, is_left_invariant_haarContent, haarContent_outerMeasure_closure_pos, haarContent_outerMeasure_self_pos
haarProduct 📖	CompOp	4 math math: mem_prehaar_empty, prehaar_mem_haarProduct, chaar_mem_haarProduct, nonempty_iInter_clPrehaar
index 📖	CompOp	11 math math: le_index_mul, index_elim, prehaar_le_index, mem_prehaar_empty, is_left_invariant_index, index_empty, index_union_eq, mul_left_index_le, index_mono, index_pos, index_union_le
prehaar 📖	CompOp	10 math math: prehaar_le_index, prehaar_sup_le, prehaar_pos, prehaar_empty, prehaar_sup_eq, prehaar_nonneg, prehaar_mono, prehaar_mem_haarProduct, prehaar_self, is_left_invariant_prehaar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addCHaar_empty 📖	mathematical	—	addCHaar Bot.bot TopologicalSpace.Compacts TopologicalSpace.Compacts.instBot Real Real.instZero	—	continuous_apply Set.mem_of_subset_of_mem IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace addPrehaar_empty addCHaar_mem_clAddPrehaar
addCHaar_mem_addHaarProduct 📖	mathematical	—	Set Set.instMembership addHaarProduct SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike addCHaar	—	nonempty_iInter_clAddPrehaar
addCHaar_mem_clAddPrehaar 📖	mathematical	—	Set Set.instMembership clAddPrehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike addCHaar	—	nonempty_iInter_clAddPrehaar Set.mem_iInter
addCHaar_mono 📖	mathematical	Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	Real Real.instLE addCHaar	—	Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_apply sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Set.mem_of_subset_of_mem IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_Ici instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Set.mem_preimage Set.mem_Ici addPrehaar_mono IsOpen.interior_eq addCHaar_mem_clAddPrehaar
addCHaar_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero addCHaar	—	addCHaar_mem_addHaarProduct Set.mem_univ Set.mem_Icc
addCHaar_self 📖	mathematical	—	addCHaar TopologicalSpace.PositiveCompacts.toCompacts Real Real.instOne	—	continuous_apply Set.mem_of_subset_of_mem IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace addPrehaar_self IsOpen.interior_eq addCHaar_mem_clAddPrehaar
addCHaar_sup_eq 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice TopologicalSpace.Compacts.carrier	addCHaar TopologicalSpace.Compacts TopologicalSpace.Compacts.instMax Real Real.instAdd	—	SeparatedNhds.of_isCompact_isCompact_isClosed instR1Space IsTopologicalAddGroup.regularSpace TopologicalSpace.Compacts.isCompact' compact_open_separated_add_right IsTopologicalAddGroup.toContinuousAdd mem_nhds_iff Set.Subset.trans Set.add_subset_add_left Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Continuous.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_apply sub_eq_zero Set.mem_of_subset_of_mem IsOpen.preimage ContinuousNeg.continuous_neg IsTopologicalAddGroup.toContinuousNeg IsOpen.inter Set.mem_neg neg_zero Set.mem_inter_iff IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Set.mem_preimage Set.mem_singleton_iff addPrehaar_sup_eq IsOpen.interior_eq Set.disjoint_of_subset Set.add_subset_add Set.Subset.rfl Set.neg_subset Set.inter_subset_left Set.inter_subset_right addCHaar_mem_clAddPrehaar
addCHaar_sup_le 📖	mathematical	—	Real Real.instLE addCHaar TopologicalSpace.Compacts TopologicalSpace.Compacts.instMax Real.instAdd	—	Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Continuous.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_apply sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Set.mem_of_subset_of_mem IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_Ici instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Set.mem_preimage Set.mem_Ici addPrehaar_sup_le IsOpen.interior_eq addCHaar_mem_clAddPrehaar
addHaarContent_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal MeasureTheory.Content.instFunLikeCompactsENNReal addHaarContent ENNReal.ofNNReal	—	—
addHaarContent_outerMeasure_closure_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.Content.outerMeasure addHaarContent closure SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	LT.lt.trans_le addHaarContent_outerMeasure_self_pos MeasureTheory.OuterMeasure.mono subset_closure
addHaarContent_outerMeasure_self_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.Content.outerMeasure addHaarContent SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	LT.lt.trans_le zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero MeasureTheory.Content.outerMeasure_eq_iInf instR1Space IsTopologicalAddGroup.regularSpace le_iInf₂ le_iInf le_trans Eq.ge addHaarContent_self le_iSup₂
addHaarContent_self 📖	mathematical	—	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal MeasureTheory.Content.instFunLikeCompactsENNReal addHaarContent TopologicalSpace.PositiveCompacts.toCompacts AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	addCHaar_nonneg addCHaar_self
addIndex_defined 📖	mathematical	IsCompact Set.Nonempty interior	Set Set.instMembership Set.image Finset Finset.card setOf Set.instHasSubset Set.iUnion Finset.instMembership Set.preimage AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	compact_covered_by_add_left_translates
addIndex_elim 📖	mathematical	IsCompact Set.Nonempty interior	Set Set.instHasSubset Set.iUnion Finset Finset.instMembership Set.preimage AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.card addIndex	—	Nat.sInf_mem addIndex_defined Set.mem_image
addIndex_empty 📖	mathematical	—	addIndex Set Set.instEmptyCollection	—	Set.empty_subset Set.image_univ Nat.sInf_eq_zero Set.mem_range Finset.card_eq_zero Set.range_eq_empty_iff not_isEmpty_of_nonempty
addIndex_mono 📖	mathematical	IsCompact Set Set.instHasSubset Set.Nonempty interior	addIndex	—	addIndex_elim Nat.sInf_le Set.mem_image Set.Subset.trans
addIndex_pos 📖	mathematical	Set.Nonempty interior	addIndex SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	addIndex.eq_1 addIndex_defined TopologicalSpace.PositiveCompacts.isCompact Nat.sInf_def Nat.find_pos Set.mem_image TopologicalSpace.PositiveCompacts.interior_nonempty Set.iUnion_congr_Prop Finset.notMem_empty Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty interior_subset Finset.card_eq_zero
addIndex_union_eq 📖	mathematical	Set.Nonempty interior Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid TopologicalSpace.Compacts.carrier Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	addIndex Set.instUnion	—	le_antisymm addIndex_union_le addIndex_elim IsCompact.union TopologicalSpace.Compacts.isCompact' Nat.sInf_le Set.mem_setOf_eq Set.mem_iUnion Finset.mem_filter Set.mem_inter_iff Set.mem_preimage le_trans add_le_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Set.Subset.trans Set.subset_union_left Set.subset_union_right Finset.card_union_of_disjoint Finset.disjoint_filter Disjoint.le_bot Set.mem_add Set.mem_neg neg_neg neg_add_rev add_neg_cancel_left Finset.filter_union_right Finset.card_filter_le
addIndex_union_le 📖	mathematical	Set.Nonempty interior	addIndex Set Set.instUnion TopologicalSpace.Compacts.carrier	—	addIndex_elim TopologicalSpace.Compacts.isCompact' le_trans Nat.sInf_le Set.mem_setOf_eq Finset.set_biUnion_union Set.union_subset_union Finset.card_union_le
addPrehaar_empty 📖	mathematical	—	addPrehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike Bot.bot TopologicalSpace.Compacts TopologicalSpace.Compacts.instBot Real Real.instZero	—	addPrehaar.eq_1 TopologicalSpace.Compacts.coe_bot addIndex_empty Nat.cast_zero zero_div
addPrehaar_mem_addHaarProduct 📖	mathematical	Set.Nonempty interior	Set Set.instMembership addHaarProduct SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike addPrehaar	—	Set.mem_Icc addPrehaar_nonneg add_prehaar_le_addIndex
addPrehaar_mono 📖	mathematical	Set.Nonempty interior Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike TopologicalSpace.Compacts.carrier	Real Real.instLE addPrehaar TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_zero Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero addIndex_pos Nat.cast_le addIndex_mono TopologicalSpace.Compacts.isCompact'
addPrehaar_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero addPrehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_zero Nat.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero zero_le Nat.instCanonicallyOrderedAdd
addPrehaar_pos 📖	mathematical	Set.Nonempty interior IsCompact	Real Real.instLT Real.instZero addPrehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_zero Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero addIndex_pos
addPrehaar_self 📖	mathematical	Set.Nonempty interior	addPrehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike TopologicalSpace.PositiveCompacts.toCompacts Real Real.instOne	—	div_self ne_of_gt Nat.cast_zero Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing addIndex_pos
addPrehaar_sup_eq 📖	mathematical	Set.Nonempty interior Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid TopologicalSpace.Compacts.carrier Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	addPrehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike TopologicalSpace.Compacts TopologicalSpace.Compacts.instMax Real Real.instAdd	—	add_div Nat.cast_add IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing addIndex_union_eq
addPrehaar_sup_le 📖	mathematical	Set.Nonempty interior	Real Real.instLE addPrehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike TopologicalSpace.Compacts TopologicalSpace.Compacts.instMax Real.instAdd	—	add_div div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_zero Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero addIndex_pos Nat.cast_add Nat.cast_le addIndex_union_le
add_left_addIndex_le 📖	mathematical	IsCompact Set.Nonempty interior	addIndex Set.image AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	addIndex_elim Nat.sInf_le Set.mem_image Set.Subset.trans Set.image_mono Set.iUnion_congr_Prop Finset.mem_map Set.mem_iUnion Set.mem_preimage exists_exists_and_eq_and add_assoc neg_add_cancel_left Finset.card_map
add_prehaar_le_addIndex 📖	mathematical	Set.Nonempty interior	Real Real.instLE addPrehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike Real.instNatCast addIndex TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	—	div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_zero Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero addIndex_pos Nat.cast_mul Nat.cast_le le_addIndex_mul
chaar_empty 📖	mathematical	—	chaar Bot.bot TopologicalSpace.Compacts TopologicalSpace.Compacts.instBot Real Real.instZero	—	continuous_apply Set.mem_of_subset_of_mem IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace prehaar_empty chaar_mem_clPrehaar
chaar_mem_clPrehaar 📖	mathematical	—	Set Set.instMembership clPrehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike chaar	—	nonempty_iInter_clPrehaar Set.mem_iInter
chaar_mem_haarProduct 📖	mathematical	—	Set Set.instMembership haarProduct SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike chaar	—	nonempty_iInter_clPrehaar
chaar_mono 📖	mathematical	Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	Real Real.instLE chaar	—	Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_apply sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Set.mem_of_subset_of_mem IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_Ici instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal prehaar_mono IsOpen.interior_eq chaar_mem_clPrehaar
chaar_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero chaar	—	chaar_mem_haarProduct Set.mem_univ Set.mem_Icc
chaar_self 📖	mathematical	—	chaar TopologicalSpace.PositiveCompacts.toCompacts Real Real.instOne	—	continuous_apply Set.mem_of_subset_of_mem IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace prehaar_self IsOpen.interior_eq chaar_mem_clPrehaar
chaar_sup_eq 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice TopologicalSpace.Compacts.carrier	chaar TopologicalSpace.Compacts TopologicalSpace.Compacts.instMax Real Real.instAdd	—	SeparatedNhds.of_isCompact_isCompact_isClosed instR1Space IsTopologicalGroup.regularSpace TopologicalSpace.Compacts.isCompact' compact_open_separated_mul_right IsTopologicalGroup.toContinuousMul mem_nhds_iff Set.Subset.trans Set.mul_subset_mul_left Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Continuous.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_apply sub_eq_zero Set.mem_of_subset_of_mem IsOpen.preimage ContinuousInv.continuous_inv IsTopologicalGroup.toContinuousInv IsOpen.inter inv_one IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace prehaar_sup_eq IsOpen.interior_eq Set.disjoint_of_subset Set.mul_subset_mul Set.Subset.rfl Set.inv_subset Set.inter_subset_left Set.inter_subset_right chaar_mem_clPrehaar
chaar_sup_le 📖	mathematical	—	Real Real.instLE chaar TopologicalSpace.Compacts TopologicalSpace.Compacts.instMax Real.instAdd	—	Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Continuous.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_apply sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Set.mem_of_subset_of_mem IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_Ici instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal prehaar_sup_le IsOpen.interior_eq chaar_mem_clPrehaar
haarContent_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal MeasureTheory.Content.instFunLikeCompactsENNReal haarContent ENNReal.ofNNReal	—	—
haarContent_outerMeasure_closure_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.Content.outerMeasure haarContent closure SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	LT.lt.trans_le haarContent_outerMeasure_self_pos MeasureTheory.OuterMeasure.mono subset_closure
haarContent_outerMeasure_self_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.Content.outerMeasure haarContent SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	LT.lt.trans_le zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero MeasureTheory.Content.outerMeasure_eq_iInf instR1Space IsTopologicalGroup.regularSpace le_iInf₂ le_iInf le_trans Eq.ge haarContent_self le_iSup₂
haarContent_self 📖	mathematical	—	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal MeasureTheory.Content.instFunLikeCompactsENNReal haarContent TopologicalSpace.PositiveCompacts.toCompacts AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	chaar_nonneg chaar_self
index_defined 📖	mathematical	IsCompact Set.Nonempty interior	Set Set.instMembership Set.image Finset Finset.card setOf Set.instHasSubset Set.iUnion Finset.instMembership Set.preimage MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	compact_covered_by_mul_left_translates
index_elim 📖	mathematical	IsCompact Set.Nonempty interior	Set Set.instHasSubset Set.iUnion Finset Finset.instMembership Set.preimage MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.card index	—	Nat.sInf_mem index_defined Set.mem_image
index_empty 📖	mathematical	—	index Set Set.instEmptyCollection	—	Set.image_univ
index_mono 📖	mathematical	IsCompact Set Set.instHasSubset Set.Nonempty interior	index	—	index_elim Nat.sInf_le Set.mem_image Set.Subset.trans
index_pos 📖	mathematical	Set.Nonempty interior	index SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	index.eq_1 index_defined TopologicalSpace.PositiveCompacts.isCompact Nat.sInf_def Nat.find_pos Set.mem_image TopologicalSpace.PositiveCompacts.interior_nonempty Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty interior_subset Finset.card_eq_zero
index_union_eq 📖	mathematical	Set.Nonempty interior Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid TopologicalSpace.Compacts.carrier Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	index Set.instUnion	—	le_antisymm index_union_le index_elim IsCompact.union TopologicalSpace.Compacts.isCompact' Nat.sInf_le Set.mem_setOf_eq le_trans add_le_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Set.Subset.trans Set.subset_union_left Set.subset_union_right Finset.card_union_of_disjoint Finset.disjoint_filter Disjoint.le_bot inv_inv mul_inv_rev mul_inv_cancel_left Finset.filter_union_right Finset.card_filter_le
index_union_le 📖	mathematical	Set.Nonempty interior	index Set Set.instUnion TopologicalSpace.Compacts.carrier	—	index_elim TopologicalSpace.Compacts.isCompact' le_trans Nat.sInf_le Set.mem_setOf_eq Finset.set_biUnion_union Set.union_subset_union Finset.card_union_le
is_left_invariant_addCHaar 📖	mathematical	—	addCHaar TopologicalSpace.Compacts.map AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid continuous_add_left IsTopologicalAddGroup.toContinuousAdd	—	continuous_add_left IsTopologicalAddGroup.toContinuousAdd Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_apply sub_eq_zero Set.mem_of_subset_of_mem IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Set.mem_preimage Set.mem_singleton_iff is_left_invariant_addPrehaar IsOpen.interior_eq addCHaar_mem_clAddPrehaar
is_left_invariant_addHaarContent 📖	mathematical	—	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal MeasureTheory.Content.instFunLikeCompactsENNReal addHaarContent TopologicalSpace.Compacts.map AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid continuous_add_left IsTopologicalAddGroup.toContinuousAdd	—	continuous_add_left IsTopologicalAddGroup.toContinuousAdd addCHaar_nonneg is_left_invariant_addCHaar
is_left_invariant_addIndex 📖	mathematical	IsCompact Set.Nonempty interior	addIndex Set.image AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	le_antisymm add_left_addIndex_le Set.image_image neg_add_cancel_left Set.image_id' IsCompact.image continuous_add_left IsTopologicalAddGroup.toContinuousAdd
is_left_invariant_addPrehaar 📖	mathematical	Set.Nonempty interior	addPrehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike TopologicalSpace.Compacts.map AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid continuous_add_left IsTopologicalAddGroup.toContinuousAdd	—	continuous_add_left IsTopologicalAddGroup.toContinuousAdd is_left_invariant_addIndex TopologicalSpace.Compacts.isCompact
is_left_invariant_chaar 📖	mathematical	—	chaar TopologicalSpace.Compacts.map MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid continuous_mul_left IsTopologicalGroup.toContinuousMul	—	continuous_mul_left IsTopologicalGroup.toContinuousMul Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_apply sub_eq_zero Set.mem_of_subset_of_mem IsClosed.closure_subset_iff continuous_iff_isClosed isClosed_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace is_left_invariant_prehaar IsOpen.interior_eq chaar_mem_clPrehaar
is_left_invariant_haarContent 📖	mathematical	—	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal MeasureTheory.Content.instFunLikeCompactsENNReal haarContent TopologicalSpace.Compacts.map MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid continuous_mul_left IsTopologicalGroup.toContinuousMul	—	continuous_mul_left IsTopologicalGroup.toContinuousMul chaar_nonneg is_left_invariant_chaar
is_left_invariant_index 📖	mathematical	IsCompact Set.Nonempty interior	index Set.image MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	le_antisymm mul_left_index_le Set.image_image inv_mul_cancel_left Set.image_id' IsCompact.image continuous_mul_left IsTopologicalGroup.toContinuousMul
is_left_invariant_prehaar 📖	mathematical	Set.Nonempty interior	prehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike TopologicalSpace.Compacts.map MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid continuous_mul_left IsTopologicalGroup.toContinuousMul	—	continuous_mul_left IsTopologicalGroup.toContinuousMul is_left_invariant_index TopologicalSpace.Compacts.isCompact
le_addIndex_mul 📖	mathematical	Set.Nonempty interior	addIndex SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	addIndex_elim TopologicalSpace.Compacts.isCompact TopologicalSpace.PositiveCompacts.interior_nonempty TopologicalSpace.PositiveCompacts.isCompact mul_comm le_trans Nat.sInf_le Set.mem_setOf_eq Set.Subset.trans Set.iUnion₂_subset Set.preimage_subset_iff Set.mem_biUnion Finset.add_mem_add add_assoc Set.mem_preimage Finset.card_add_le
le_index_mul 📖	mathematical	Set.Nonempty interior	index SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	index_elim TopologicalSpace.Compacts.isCompact TopologicalSpace.PositiveCompacts.interior_nonempty TopologicalSpace.PositiveCompacts.isCompact mul_comm le_trans Nat.sInf_le Set.mem_setOf_eq Set.Subset.trans Set.iUnion₂_subset Set.preimage_subset_iff Set.mem_biUnion Finset.mul_mem_mul mul_assoc Set.mem_preimage Finset.card_mul_le
mem_addPrehaar_empty 📖	mathematical	—	Set Set.instMembership addHaarProduct Real Set.Icc Real.instPreorder Real.instZero Real.instNatCast addIndex SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	—	Set.mem_univ
mem_prehaar_empty 📖	mathematical	—	Set Set.instMembership haarProduct Real Set.Icc Real.instPreorder Real.instZero Real.instNatCast index SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	—	—
mul_left_index_le 📖	mathematical	IsCompact Set.Nonempty interior	index Set.image MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	index_elim Nat.sInf_le Set.mem_image Set.Subset.trans Set.image_mono Set.iUnion_congr_Prop mul_assoc inv_mul_cancel_left Finset.card_map
nonempty_iInter_clAddPrehaar 📖	mathematical	—	Set.Nonempty Set Set.instInter addHaarProduct SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike Set.iInter TopologicalSpace.OpenNhdsOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid clAddPrehaar	—	isCompact_univ_pi CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal IsCompact.inter_iInter_nonempty isClosed_closure isOpen_biInter_finset Set.mem_iInter addPrehaar_mem_addHaarProduct IsOpen.interior_eq subset_closure Set.mem_image_of_mem Set.mem_setOf_eq Set.Subset.trans Set.iInter_subset
nonempty_iInter_clPrehaar 📖	mathematical	—	Set.Nonempty Set Set.instInter haarProduct SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike Set.iInter TopologicalSpace.OpenNhdsOf InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid clPrehaar	—	isCompact_univ_pi CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal IsCompact.inter_iInter_nonempty isClosed_closure isOpen_biInter_finset prehaar_mem_haarProduct IsOpen.interior_eq subset_closure Set.mem_image_of_mem Set.mem_setOf_eq Set.Subset.trans Set.iInter_subset
prehaar_empty 📖	mathematical	—	prehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike Bot.bot TopologicalSpace.Compacts TopologicalSpace.Compacts.instBot Real Real.instZero	—	prehaar.eq_1 TopologicalSpace.Compacts.coe_bot index_empty Nat.cast_zero zero_div
prehaar_le_index 📖	mathematical	Set.Nonempty interior	Real Real.instLE prehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike Real.instNatCast index TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	—	div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero index_pos le_index_mul
prehaar_mem_haarProduct 📖	mathematical	Set.Nonempty interior	Set Set.instMembership haarProduct SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike prehaar	—	Set.mem_Icc prehaar_nonneg prehaar_le_index
prehaar_mono 📖	mathematical	Set.Nonempty interior Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike TopologicalSpace.Compacts.carrier	Real Real.instLE prehaar TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero index_pos index_mono TopologicalSpace.Compacts.isCompact'
prehaar_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero prehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero zero_le Nat.instCanonicallyOrderedAdd
prehaar_pos 📖	mathematical	Set.Nonempty interior IsCompact	Real Real.instLT Real.instZero prehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike	—	div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero index_pos
prehaar_self 📖	mathematical	Set.Nonempty interior	prehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike TopologicalSpace.PositiveCompacts.toCompacts Real Real.instOne	—	div_self ne_of_gt Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing index_pos
prehaar_sup_eq 📖	mathematical	Set.Nonempty interior Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid TopologicalSpace.Compacts.carrier Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	prehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike TopologicalSpace.Compacts TopologicalSpace.Compacts.instMax Real Real.instAdd	—	add_div IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing index_union_eq
prehaar_sup_le 📖	mathematical	Set.Nonempty interior	Real Real.instLE prehaar SetLike.coe TopologicalSpace.PositiveCompacts TopologicalSpace.PositiveCompacts.instSetLike TopologicalSpace.Compacts TopologicalSpace.Compacts.instMax Real.instAdd	—	add_div div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero index_pos index_union_le

---

← Back to Index