Documentation Verification Report

OfMinimal

📁 Source: Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean

Statistics

Metric	Count
Definitions	0
Theorems `ergodic_of_dense_iUnion_preimage_zero`, `preErgodic_of_dense_iUnion_preimage_zero`, `zpow_of_ergodic_mul_left`, `zsmul_of_ergodic_add_left`, `trans_isMinimal`, `trans_isMinimal`, `ergodic_of_dense_iUnion_preimage_one`, `preErgodic_of_dense_iUnion_preimage_one`, `aeconst_of_dense_aestabilizer_smul`, `aeconst_of_dense_aestabilizer_vadd`, `aeconst_of_dense_setOf_preimage_smul_ae`, `aeconst_of_dense_setOf_preimage_smul_eq`, `aeconst_of_dense_setOf_preimage_vadd_ae`, `aeconst_of_dense_setOf_preimage_vadd_eq`, `ergodic_add_left_iff_denseRange_zsmul`, `ergodic_add_left_of_denseRange_nsmul`, `ergodic_add_left_of_denseRange_zsmul`, `ergodic_mul_left_iff_denseRange_zpow`, `ergodic_mul_left_of_denseRange_pow`, `ergodic_mul_left_of_denseRange_zpow`, `ergodic_smul_of_denseRange_pow`, `ergodic_smul_of_denseRange_zpow`, `ergodic_vadd_of_denseRange_nsmul`, `ergodic_vadd_of_denseRange_zsmul`	24
Total	24

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ergodic_of_dense_iUnion_preimage_zero` 📖	mathematical	`Dense` `Set.iUnion` `Set.preimage` `Nat.iterate` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `Set` `Set.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Continuous`	`Ergodic`	—	`measurePreserving` `preErgodic_of_dense_iUnion_preimage_zero` `MeasureTheory.CompactSpace.isFiniteMeasure` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.instInnerRegularOfIsAddHaarMeasureOfCompactSpace` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant`
`preErgodic_of_dense_iUnion_preimage_zero` 📖	mathematical	`Dense` `Set.iUnion` `Set.preimage` `Nat.iterate` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `Set` `Set.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`PreErgodic`	—	`aeconst_of_dense_setOf_preimage_vadd_eq` `instR1Space` `IsTopologicalAddGroup.regularSpace` `ContinuousAdd.to_continuousVAdd` `IsTopologicalAddGroup.toContinuousAdd` `instErgodicVAddOfIsAddLeftInvariant` `ContinuousAdd.measurableMul₂` `ContinuousNeg.measurableNeg` `IsTopologicalAddGroup.toContinuousNeg` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasurableSet.nullMeasurableSet` `Dense.mono` `Set.iUnion_subset` `Set.preimage_iterate_eq` `Function.iterate_fixed` `Set.mem_setOf` `Set.ext` `Set.mem_preimage` `iterate_map_add` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass` `Set.mem_zero` `zero_add`

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zpow_of_ergodic_mul_left` 📖	mathematical	`Ergodic` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`DenseRange` `DivInvMonoid.toZPow`	—	`Continuous.tendsto'` `Continuous.div'` `IsTopologicalGroup.to_continuousDiv` `Continuous.comp'` `Continuous.fun_mul` `IsTopologicalGroup.toContinuousMul` `continuous_const` `continuous_id'` `Continuous.fst` `Continuous.snd` `mul_one` `div_one` `Filter.HasBasis.mem_iff` `Filter.HasBasis.prod_self` `nhds_basis_opens` `nhds_prod_eq` `mem_interior_iff_mem_nhds` `interior_compl` `Set.mem_compl_iff` `isOpen_iUnion` `IsOpen.smul` `IsScalarTower.continuousConstSMul` `IsScalarTower.left` `Set.mem_iUnion` `zpow_zero` `one_smul` `mul_div_cancel_right` `Set.preimage_iUnion` `Set.preimage_smul` `Set.iUnion_congr_of_surjective` `add_left_surjective` `zpow_add` `zpow_neg` `zpow_one` `SemigroupAction.mul_smul` `PreErgodic.measure_self_or_compl_eq_zero` `Ergodic.toPreErgodic` `IsOpen.measurableSet` `IsOpen.measure_ne_zero` `Set.Nonempty.image` `MeasureTheory.measure_mono_null` `MeasureTheory.Measure.instOuterMeasureClass` `Set.disjoint_right`
`zsmul_of_ergodic_add_left` 📖	mathematical	`Ergodic` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`DenseRange` `SubNegMonoid.toZSMul`	—	`Continuous.tendsto'` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `Continuous.comp'` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `continuous_const` `continuous_id'` `Continuous.fst` `Continuous.snd` `add_zero` `sub_zero` `Filter.mem_map` `Filter.HasBasis.mem_iff` `Filter.HasBasis.prod_self` `nhds_basis_opens` `Set.prod_subset_iff` `Set.mem_compl_iff` `Set.mem_preimage` `Set.mem_range` `nhds_prod_eq` `mem_interior_iff_mem_nhds` `interior_compl` `isOpen_iUnion` `IsOpen.vadd` `VAddAssocClass.continuousConstVAdd` `VAddAssocClass.left` `Set.mem_iUnion` `zero_zsmul` `zero_vadd` `Set.disjoint_iUnion_left` `Set.disjoint_left` `add_sub_cancel_right` `Set.preimage_iUnion` `Set.preimage_vadd` `Set.iUnion_congr_of_surjective` `add_left_surjective` `add_zsmul` `neg_zsmul` `one_zsmul` `AddSemigroupAction.add_vadd` `PreErgodic.measure_self_or_compl_eq_zero` `Ergodic.toPreErgodic` `IsOpen.measurableSet` `IsOpen.measure_ne_zero` `Set.Nonempty.image` `MeasureTheory.measure_mono_null` `MeasureTheory.Measure.instOuterMeasureClass` `Set.disjoint_right`

ErgodicSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans_isMinimal` 📖	mathematical	—	`ErgodicSMul`	—	`smul_one_smul` `MeasureTheory.SMulInvariantMeasure.measure_preimage_smul` `toSMulInvariantMeasure` `MeasureTheory.Measure.instOuterMeasureClass` `aeconst_of_dense_setOf_preimage_smul_ae` `MeasurableSet.nullMeasurableSet` `Dense.mono` `smul_assoc` `one_smul` `MulAction.dense_orbit`

ErgodicVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans_isMinimal` 📖	mathematical	—	`ErgodicVAdd`	—	`vadd_zero_vadd` `MeasureTheory.VAddInvariantMeasure.measure_preimage_vadd` `toVAddInvariantMeasure` `MeasureTheory.Measure.instOuterMeasureClass` `aeconst_of_dense_setOf_preimage_vadd_ae` `MeasurableSet.nullMeasurableSet` `Dense.mono` `vadd_assoc` `zero_vadd` `AddAction.dense_orbit`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ergodic_of_dense_iUnion_preimage_one` 📖	mathematical	`Dense` `Set.iUnion` `Set.preimage` `Nat.iterate` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `Set` `Set.one` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Continuous`	`Ergodic`	—	`measurePreserving` `preErgodic_of_dense_iUnion_preimage_one` `MeasureTheory.CompactSpace.isFiniteMeasure` `MeasureTheory.Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.instInnerRegularOfIsHaarMeasureOfCompactSpace` `MeasureTheory.Measure.IsHaarMeasure.toIsMulLeftInvariant`
`preErgodic_of_dense_iUnion_preimage_one` 📖	mathematical	`Dense` `Set.iUnion` `Set.preimage` `Nat.iterate` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `Set` `Set.one` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`PreErgodic`	—	`aeconst_of_dense_setOf_preimage_smul_eq` `instR1Space` `IsTopologicalGroup.regularSpace` `ContinuousMul.to_continuousSMul` `IsTopologicalGroup.toContinuousMul` `instErgodicSMulOfIsMulLeftInvariant` `ContinuousMul.measurableMul₂` `ContinuousInv.measurableInv` `IsTopologicalGroup.toContinuousInv` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasurableSet.nullMeasurableSet` `Dense.mono` `Set.iUnion_subset` `Set.preimage_iterate_eq` `Function.iterate_fixed` `Set.mem_setOf` `Set.ext` `iterate_map_mul` `MonoidHomClass.toMulHomClass` `instMonoidHomClass` `Set.mem_one` `Set.mem_preimage` `one_mul`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeconst_of_dense_aestabilizer_smul` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `Dense` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MulAction.aestabilizer` `ErgodicSMul.toSMulInvariantMeasure` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`Filter.EventuallyConst` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`ErgodicSMul.toSMulInvariantMeasure` `aeconst_of_dense_setOf_preimage_smul_ae` `Dense.mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.preimage_smul` `Dense.preimage` `isOpenMap_inv`
`aeconst_of_dense_aestabilizer_vadd` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `Dense` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddAction.aestabilizer` `ErgodicVAdd.toVAddInvariantMeasure` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`Filter.EventuallyConst` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`ErgodicVAdd.toVAddInvariantMeasure` `aeconst_of_dense_setOf_preimage_vadd_ae` `Dense.mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.preimage_vadd` `Dense.preimage` `isOpenMap_neg`
`aeconst_of_dense_setOf_preimage_smul_ae` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `Dense` `setOf` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Set.preimage`	`Filter.EventuallyConst`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.aeconst_of_forall_preimage_smul_ae_eq` `Set.eq_univ_iff_forall` `IsClosed.closure_eq` `ContinuousSMul.continuous_smul` `MeasureTheory.isClosed_setOf_preimage_ae_eq` `MeasureTheory.Measure.InnerRegular.instInnerRegularCompactLTTop` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `ContinuousMap.continuous` `MeasureTheory.measurePreserving_smul` `MeasurableSMul.toMeasurableConstSMul` `ContinuousSMul.toMeasurableSMul` `BorelSpace.opensMeasurable` `ErgodicSMul.toSMulInvariantMeasure` `MeasureTheory.measure_ne_top` `dense_iff_closure_eq`
`aeconst_of_dense_setOf_preimage_smul_eq` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `Dense` `setOf` `Set` `Set.preimage`	`Filter.EventuallyConst` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`aeconst_of_dense_setOf_preimage_smul_ae` `Dense.mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.mem_setOf` `Filter.EventuallyEq.of_eq`
`aeconst_of_dense_setOf_preimage_vadd_ae` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `Dense` `setOf` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Set.preimage` `HVAdd.hVAdd` `instHVAdd`	`Filter.EventuallyConst`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.aeconst_of_forall_preimage_vadd_ae_eq` `Set.eq_univ_iff_forall` `IsClosed.closure_eq` `ContinuousVAdd.continuous_vadd` `MeasureTheory.isClosed_setOf_preimage_ae_eq` `MeasureTheory.Measure.InnerRegular.instInnerRegularCompactLTTop` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `ContinuousMap.continuous` `MeasureTheory.measurePreserving_vadd` `MeasurableVAdd.toMeasurableConstVAdd` `ContinuousVAdd.toMeasurableVAdd` `BorelSpace.opensMeasurable` `ErgodicVAdd.toVAddInvariantMeasure` `MeasureTheory.measure_ne_top` `dense_iff_closure_eq`
`aeconst_of_dense_setOf_preimage_vadd_eq` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `Dense` `setOf` `Set` `Set.preimage` `HVAdd.hVAdd` `instHVAdd`	`Filter.EventuallyConst` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`aeconst_of_dense_setOf_preimage_vadd_ae` `Dense.mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.mem_setOf` `Filter.EventuallyEq.of_eq`
`ergodic_add_left_iff_denseRange_zsmul` 📖	mathematical	—	`Ergodic` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DenseRange` `SubNegMonoid.toZSMul`	—	`DenseRange.zsmul_of_ergodic_add_left` `BorelSpace.opensMeasurable` `MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_innerRegular` `ergodic_add_left_of_denseRange_zsmul`
`ergodic_add_left_of_denseRange_nsmul` 📖	mathematical	`DenseRange` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`Ergodic` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`ergodic_vadd_of_denseRange_nsmul` `instR1Space` `IsTopologicalAddGroup.regularSpace` `ContinuousAdd.to_continuousVAdd` `IsTopologicalAddGroup.toContinuousAdd` `instErgodicVAddOfIsAddLeftInvariant` `ContinuousAdd.measurableMul₂` `ContinuousNeg.measurableNeg` `IsTopologicalAddGroup.toContinuousNeg` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure`
`ergodic_add_left_of_denseRange_zsmul` 📖	mathematical	`DenseRange` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	`Ergodic` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`ergodic_vadd_of_denseRange_zsmul` `IsTopologicalAddGroup.toContinuousNeg` `instR1Space` `IsTopologicalAddGroup.regularSpace` `ContinuousAdd.to_continuousVAdd` `IsTopologicalAddGroup.toContinuousAdd` `instErgodicVAddOfIsAddLeftInvariant` `ContinuousAdd.measurableMul₂` `ContinuousNeg.measurableNeg` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure`
`ergodic_mul_left_iff_denseRange_zpow` 📖	mathematical	—	`Ergodic` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DenseRange` `DivInvMonoid.toZPow`	—	`DenseRange.zpow_of_ergodic_mul_left` `BorelSpace.opensMeasurable` `MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_innerRegular` `ergodic_mul_left_of_denseRange_zpow`
`ergodic_mul_left_of_denseRange_pow` 📖	mathematical	`DenseRange` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`Ergodic` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`ergodic_smul_of_denseRange_pow` `instR1Space` `IsTopologicalGroup.regularSpace` `ContinuousMul.to_continuousSMul` `IsTopologicalGroup.toContinuousMul` `instErgodicSMulOfIsMulLeftInvariant` `ContinuousMul.measurableMul₂` `ContinuousInv.measurableInv` `IsTopologicalGroup.toContinuousInv` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure`
`ergodic_mul_left_of_denseRange_zpow` 📖	mathematical	`DenseRange` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	`Ergodic` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`ergodic_smul_of_denseRange_zpow` `IsTopologicalGroup.toContinuousInv` `instR1Space` `IsTopologicalGroup.regularSpace` `ContinuousMul.to_continuousSMul` `IsTopologicalGroup.toContinuousMul` `instErgodicSMulOfIsMulLeftInvariant` `ContinuousMul.measurableMul₂` `ContinuousInv.measurableInv` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure`
`ergodic_smul_of_denseRange_pow` 📖	mathematical	`DenseRange` `Monoid.toNatPow`	`Ergodic` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`MeasureTheory.measurePreserving_smul` `MeasurableSMul.toMeasurableConstSMul` `ContinuousSMul.toMeasurableSMul` `BorelSpace.opensMeasurable` `ErgodicSMul.toSMulInvariantMeasure` `aeconst_of_dense_setOf_preimage_smul_eq` `MeasurableSet.nullMeasurableSet` `Dense.mono` `Set.range_subset_iff` `Set.mem_setOf` `smul_iterate` `Set.preimage_iterate_eq` `Function.iterate_fixed`
`ergodic_smul_of_denseRange_zpow` 📖	mathematical	`DenseRange` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	`Ergodic` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `MulAction.toSemigroupAction`	—	`MeasureTheory.measurePreserving_smul` `MeasurableSMul.toMeasurableConstSMul` `ContinuousSMul.toMeasurableSMul` `BorelSpace.opensMeasurable` `ErgodicSMul.toSMulInvariantMeasure` `aeconst_of_dense_aestabilizer_smul` `MeasurableSet.nullMeasurableSet` `Dense.mono` `Subgroup.coe_zpowers` `SetLike.coe_subset_coe` `instIsConcreteLE` `Subgroup.zpowers_inv` `Subgroup.zpowers_le` `MeasureTheory.Measure.instOuterMeasureClass` `MulAction.mem_aestabilizer` `Set.preimage_smul` `Filter.EventuallyEq.refl`
`ergodic_vadd_of_denseRange_nsmul` 📖	mathematical	`DenseRange` `AddMonoid.toNatSMul`	`Ergodic` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	—	`MeasureTheory.measurePreserving_vadd` `MeasurableVAdd.toMeasurableConstVAdd` `ContinuousVAdd.toMeasurableVAdd` `BorelSpace.opensMeasurable` `ErgodicVAdd.toVAddInvariantMeasure` `aeconst_of_dense_setOf_preimage_vadd_eq` `MeasurableSet.nullMeasurableSet` `Dense.mono` `Set.range_subset_iff` `Set.mem_setOf` `vadd_iterate` `Set.preimage_iterate_eq` `Function.iterate_fixed`
`ergodic_vadd_of_denseRange_zsmul` 📖	mathematical	`DenseRange` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	`Ergodic` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddAction.toAddSemigroupAction`	—	`MeasureTheory.measurePreserving_vadd` `MeasurableVAdd.toMeasurableConstVAdd` `ContinuousVAdd.toMeasurableVAdd` `BorelSpace.opensMeasurable` `ErgodicVAdd.toVAddInvariantMeasure` `aeconst_of_dense_aestabilizer_vadd` `MeasurableSet.nullMeasurableSet` `Dense.mono` `AddSubgroup.coe_zmultiples` `SetLike.coe_subset_coe` `instIsConcreteLE` `AddSubgroup.zmultiples_neg` `AddSubgroup.zmultiples_le` `MeasureTheory.Measure.instOuterMeasureClass` `AddAction.mem_aestabilizer` `Set.preimage_vadd` `Filter.EventuallyEq.refl`

---

← Back to Index