AEStabilizer

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

Statistics

Metric	Count
Definitions aestabilizer, aestabilizer	2
Theorems aestabilizer_congr, aestabilizer_empty, aestabilizer_univ, coe_aestabilizer, mem_aestabilizer, stabilizer_le_aestabilizer, inv_smul_ae_eq_self, neg_vadd_ae_eq_self, smul_ae_eq_self_of_mem_zpowers, vadd_ae_eq_self_of_mem_zmultiples, aestabilizer_congr, aestabilizer_empty, aestabilizer_of_aeconst, aestabilizer_univ, coe_aestabilizer, mem_aestabilizer, stabilizer_le_aestabilizer	17
Total	19

AddAction

Definitions

Name	Category	Theorems
aestabilizer 📖	CompOp	6 math math: aestabilizer_congr, aestabilizer_empty, stabilizer_le_aestabilizer, aestabilizer_univ, coe_aestabilizer, mem_aestabilizer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestabilizer_congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	aestabilizer	—	MeasureTheory.Measure.instOuterMeasureClass AddSubgroup.ext mem_aestabilizer Filter.EventuallyEq.congr_right Filter.EventuallyEq.congr_left MeasureTheory.vadd_set_ae_eq
aestabilizer_empty 📖	mathematical	—	aestabilizer Set Set.instEmptyCollection Top.top AddSubgroup AddSubgroup.instTop	—	top_unique MeasureTheory.Measure.instOuterMeasureClass mem_aestabilizer Set.vadd_set_empty Filter.EventuallyEq.refl
aestabilizer_univ 📖	mathematical	—	aestabilizer Set.univ Top.top AddSubgroup AddSubgroup.instTop	—	top_unique MeasureTheory.Measure.instOuterMeasureClass mem_aestabilizer Set.vadd_set_univ MeasureTheory.ae_eq_univ Set.compl_univ MeasureTheory.measure_empty
coe_aestabilizer 📖	mathematical	—	SetLike.coe AddSubgroup AddSubgroup.instSetLike aestabilizer setOf Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction	—	—
mem_aestabilizer 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike aestabilizer Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction	—	—
stabilizer_le_aestabilizer 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid aestabilizer	—	MeasureTheory.Measure.instOuterMeasureClass mem_aestabilizer mem_stabilizer_iff Filter.EventuallyEq.refl

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_smul_ae_eq_self 📖	mathematical	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Measure.instOuterMeasureClass InvMemClass.inv_mem SubgroupClass.toInvMemClass Subgroup.instSubgroupClass
neg_vadd_ae_eq_self 📖	mathematical	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Measure.instOuterMeasureClass NegMemClass.neg_mem AddSubgroupClass.toNegMemClass AddSubgroup.instAddSubgroupClass
smul_ae_eq_self_of_mem_zpowers 📖	mathematical	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	Measure.instOuterMeasureClass Subgroup.zpowers_le MulAction.mem_aestabilizer
vadd_ae_eq_self_of_mem_zmultiples 📖	mathematical	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	Measure.instOuterMeasureClass AddSubgroup.zmultiples_le AddAction.mem_aestabilizer

MulAction

Definitions

Name	Category	Theorems
aestabilizer 📖	CompOp	7 math math: mem_aestabilizer, stabilizer_le_aestabilizer, aestabilizer_empty, coe_aestabilizer, aestabilizer_of_aeconst, aestabilizer_congr, aestabilizer_univ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestabilizer_congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	aestabilizer	—	MeasureTheory.Measure.instOuterMeasureClass Subgroup.ext mem_aestabilizer Filter.EventuallyEq.congr_right Filter.EventuallyEq.congr_left MeasureTheory.smul_set_ae_eq
aestabilizer_empty 📖	mathematical	—	aestabilizer Set Set.instEmptyCollection Top.top Subgroup Subgroup.instTop	—	top_unique MeasureTheory.Measure.instOuterMeasureClass Set.smul_set_empty
aestabilizer_of_aeconst 📖	mathematical	Filter.EventuallyConst MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	aestabilizer Top.top Subgroup Subgroup.instTop	—	MeasureTheory.Measure.instOuterMeasureClass top_unique Filter.eventuallyConst_set' aestabilizer_congr aestabilizer_empty aestabilizer_univ
aestabilizer_univ 📖	mathematical	—	aestabilizer Set.univ Top.top Subgroup Subgroup.instTop	—	top_unique MeasureTheory.Measure.instOuterMeasureClass Set.smul_set_univ Set.compl_univ MeasureTheory.measure_empty
coe_aestabilizer 📖	mathematical	—	SetLike.coe Subgroup Subgroup.instSetLike aestabilizer setOf Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction	—	—
mem_aestabilizer 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike aestabilizer Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction	—	—
stabilizer_le_aestabilizer 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid aestabilizer	—	MeasureTheory.Measure.instOuterMeasureClass

---

← Back to Index