CoverEntropy

📁 Source: Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean

Statistics

Metric	Count
Definitions IsDynCoverOf, coverEntropy, coverEntropyEntourage, coverEntropyInf, coverEntropyInfEntourage, coverMincard	6
Theorems coverEntropyEntourage_le_log_card_div, coverMincard_le_card, iterate_le_pow, nonempty, nonempty_inter, of_entourage_subset, of_le, coverEntropyEntourage_antitone, coverEntropyEntourage_empty, coverEntropyEntourage_finite_of_isCompact_invariant, coverEntropyEntourage_le_coverEntropy, coverEntropyEntourage_le_coverEntropyInfEntourage, coverEntropyEntourage_le_log_coverMincard_div, coverEntropyEntourage_nonneg, coverEntropyEntourage_univ, coverEntropyInfEntourage_antitone, coverEntropyInfEntourage_empty, coverEntropyInfEntourage_le_coverEntropyEntourage, coverEntropyInfEntourage_le_coverEntropyInf, coverEntropyInfEntourage_nonneg, coverEntropyInfEntourage_univ, coverEntropyInf_antitone, coverEntropyInf_empty, coverEntropyInf_eq_coverEntropy, coverEntropyInf_eq_iSup_basis, coverEntropyInf_le_coverEntropy, coverEntropyInf_nonneg, coverEntropy_antitone, coverEntropy_empty, coverEntropy_eq_iSup_basis, coverEntropy_nonneg, coverMincard_antitone, coverMincard_empty, coverMincard_eq_zero_iff, coverMincard_finite_iff, coverMincard_finite_of_isCompact_invariant, coverMincard_finite_of_isCompact_uniformContinuous, coverMincard_le_pow, coverMincard_monotone_time, coverMincard_mul_le_pow, coverMincard_univ, coverMincard_zero, exists_isDynCoverOf_of_isCompact_invariant, exists_isDynCoverOf_of_isCompact_uniformContinuous, isDynCoverOf_empty, isDynCoverOf_empty_right, isDynCoverOf_univ, isDynCoverOf_zero, nonempty_inter_of_coverMincard, one_le_coverMincard_iff	50
Total	56

Dynamics

Definitions

Name	Category	Theorems
IsDynCoverOf 📖	MathDef	7 math math: isDynCoverOf_univ, isDynCoverOf_empty, isDynCoverOf_zero, exists_isDynCoverOf_of_isCompact_uniformContinuous, coverMincard_finite_iff, isDynCoverOf_empty_right, exists_isDynCoverOf_of_isCompact_invariant
coverEntropy 📖	CompOp	22 math math: coverEntropy_restrict, coverEntropy_iUnion_le, coverEntropy_monotone, coverEntropy_union, coverEntropy_restrict_subset, coverEntropy_biUnion_finset, coverEntropy_antitone, coverEntropy_iUnion_of_finite, coverEntropy_image_le_of_uniformContinuousOn_invariant, coverEntropy_image_le_of_uniformContinuous, coverEntropy_nonneg, coverEntropy_eq_iSup_basis, coverEntropy_closure, coverEntropy_eq_iSup_basis_netEntropyEntourage, coverEntropy_biUnion_le, coverEntropy_eq_iSup_netEntropyEntourage, coverEntropyEntourage_le_coverEntropy, netEntropyEntourage_le_coverEntropy, coverEntropy_image_of_comap, coverEntropy_empty, coverEntropyInf_le_coverEntropy, coverEntropyInf_eq_coverEntropy
coverEntropyEntourage 📖	CompOp	18 math math: coverEntropyEntourage_le_coverEntropyInfEntourage, netEntropyEntourage_le_coverEntropyEntourage, coverEntropyEntourage_univ, coverEntropyEntourage_union, coverEntropyEntourage_le_netEntropyEntourage, coverEntropyInfEntourage_le_coverEntropyEntourage, coverEntropyEntourage_image_le, le_coverEntropyEntourage_image, coverEntropyEntourage_monotone, IsDynCoverOf.coverEntropyEntourage_le_log_card_div, coverEntropyEntourage_finite_of_isCompact_invariant, coverEntropyEntourage_le_log_coverMincard_div, coverEntropyEntourage_antitone, coverEntropy_eq_iSup_basis, coverEntropyEntourage_nonneg, coverEntropyEntourage_closure, coverEntropyEntourage_le_coverEntropy, coverEntropyEntourage_empty
coverEntropyInf 📖	CompOp	18 math math: coverEntropyInf_image_of_comap, coverEntropyInf_closure, coverEntropyInf_eq_iSup_netEntropyInfEntourage, coverEntropyInfEntourage_le_coverEntropyInf, coverEntropyInf_image_le_of_uniformContinuous, coverEntropyInf_monotone, coverEntropyInf_nonneg, coverEntropyInf_antitone, coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage, netEntropyInfEntourage_le_coverEntropyInf, coverEntropyInf_iUnion_le, coverEntropyInf_empty, coverEntropyInf_biUnion_le, coverEntropyInf_image_le_of_uniformContinuousOn_invariant, coverEntropyInf_eq_iSup_basis, coverEntropyInf_le_coverEntropy, coverEntropyInf_restrict_subset, coverEntropyInf_eq_coverEntropy
coverEntropyInfEntourage 📖	CompOp	14 math math: coverEntropyInfEntourage_le_netEntropyInfEntourage, coverEntropyEntourage_le_coverEntropyInfEntourage, coverEntropyInfEntourage_antitone, coverEntropyInfEntourage_univ, coverEntropyInfEntourage_le_coverEntropyInf, coverEntropyInfEntourage_le_coverEntropyEntourage, netEntropyInfEntourage_le_coverEntropyInfEntourage, coverEntropyInfEntourage_image_le, coverEntropyInfEntourage_closure, le_coverEntropyInfEntourage_image, coverEntropyInfEntourage_nonneg, coverEntropyInfEntourage_empty, coverEntropyInf_eq_iSup_basis, coverEntropyInfEntourage_monotone
coverMincard 📖	CompOp	21 math math: coverMincard_eq_zero_iff, netMaxcard_le_coverMincard, coverMincard_finite_of_isCompact_invariant, coverMincard_image_le, coverMincard_univ, coverMincard_empty, one_le_coverMincard_iff, coverMincard_monotone_time, coverMincard_closure_le, coverMincard_finite_of_isCompact_uniformContinuous, IsDynCoverOf.coverMincard_le_card, coverMincard_antitone, coverMincard_zero, coverMincard_union_le, coverEntropyEntourage_le_log_coverMincard_div, coverMincard_le_pow, coverMincard_mul_le_pow, coverMincard_le_netMaxcard, coverMincard_finite_iff, le_coverMincard_image, coverMincard_monotone_subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coverEntropyEntourage_antitone 📖	mathematical	—	Antitone SetRel EReal PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrderEReal coverEntropyEntourage	—	ExpGrowth.expGrowthSup_monotone ENat.toENNReal_mono coverMincard_antitone
coverEntropyEntourage_empty 📖	mathematical	—	coverEntropyEntourage Set Set.instEmptyCollection Bot.bot EReal instBotEReal	—	coverMincard_empty ENat.toENNReal_zero Pi.zero_def ExpGrowth.expGrowthSup_zero
coverEntropyEntourage_finite_of_isCompact_invariant 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace Set.MapsTo SetRel Filter Filter.instMembership uniformity	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal coverEntropyEntourage Top.top EReal.instTop	—	comp_symm_mem_uniformity_sets exists_isDynCoverOf_of_isCompact_invariant LE.le.trans_lt coverEntropyEntourage_antitone IsDynCoverOf.coverEntropyEntourage_le_log_card_div one_ne_zero Nat.cast_one div_one ENNReal.log_lt_top_iff ENat.toENNReal_top Ne.lt_top ENat.coe_ne_top
coverEntropyEntourage_le_coverEntropy 📖	mathematical	SetRel Filter Filter.instMembership uniformity	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal coverEntropyEntourage coverEntropy	—	le_iSup₂
coverEntropyEntourage_le_coverEntropyInfEntourage 📖	mathematical	Set.MapsTo	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal coverEntropyEntourage SetRel.comp coverEntropyInfEntourage	—	Filter.le_liminf_of_le Filter.isCobounded_ge_of_top Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat coverEntropyEntourage_le_log_coverMincard_div
coverEntropyEntourage_le_log_coverMincard_div 📖	mathematical	Set.MapsTo	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal coverEntropyEntourage SetRel.comp DivInvMonoid.toDiv EReal.instDivInvMonoid ENNReal.log ENat.toENNReal coverMincard AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	ENat.toENNReal_mono coverMincard_monotone_time Monotone.expGrowthSup_comp_mul coverEntropyEntourage.eq_1 EReal.div_eq_iff EReal.natCast_ne_bot EReal.natCast_ne_top Nat.cast_ne_zero instCharZeroEReal mul_comm EReal.monotone_div_right_of_nonneg Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal ExpGrowth.expGrowthSup_pow ExpGrowth.expGrowthSup_monotone ENat.toENNReal_pow coverMincard_mul_le_pow
coverEntropyEntourage_nonneg 📖	mathematical	Set.Nonempty	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal coverEntropyEntourage	—	LE.le.trans coverEntropyInfEntourage_nonneg coverEntropyInfEntourage_le_coverEntropyEntourage
coverEntropyEntourage_univ 📖	mathematical	Set.Nonempty	coverEntropyEntourage Set.univ EReal instZeroEReal	—	ExpGrowth.expGrowthSup_const one_ne_zero NeZero.charZero_one ENNReal.instCharZero ENNReal.one_ne_top coverEntropyEntourage.eq_1 coverMincard_univ ENat.toENNReal_one
coverEntropyInfEntourage_antitone 📖	mathematical	—	Antitone SetRel EReal PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrderEReal coverEntropyInfEntourage	—	ExpGrowth.expGrowthInf_monotone ENat.toENNReal_mono coverMincard_antitone
coverEntropyInfEntourage_empty 📖	mathematical	—	coverEntropyInfEntourage Set Set.instEmptyCollection Bot.bot EReal instBotEReal	—	eq_bot_mono coverEntropyInfEntourage_le_coverEntropyEntourage coverEntropyEntourage_empty
coverEntropyInfEntourage_le_coverEntropyEntourage 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal coverEntropyInfEntourage coverEntropyEntourage	—	ExpGrowth.expGrowthInf_le_expGrowthSup
coverEntropyInfEntourage_le_coverEntropyInf 📖	mathematical	SetRel Filter Filter.instMembership uniformity	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal coverEntropyInfEntourage coverEntropyInf	—	le_iSup₂
coverEntropyInfEntourage_nonneg 📖	mathematical	Set.Nonempty	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal coverEntropyInfEntourage	—	Monotone.expGrowthInf_nonneg ENat.toENNReal_mono coverMincard_monotone_time Iff.not coverMincard_zero Pi.zero_apply ENat.toENNReal_one one_ne_zero NeZero.charZero_one ENNReal.instCharZero
coverEntropyInfEntourage_univ 📖	mathematical	Set.Nonempty	coverEntropyInfEntourage Set.univ EReal instZeroEReal	—	ExpGrowth.expGrowthInf_const one_ne_zero NeZero.charZero_one ENNReal.instCharZero ENNReal.one_ne_top coverEntropyInfEntourage.eq_1 coverMincard_univ ENat.toENNReal_one
coverEntropyInf_antitone 📖	mathematical	—	Antitone UniformSpace EReal PartialOrder.toPreorder instPartialOrderUniformSpace instPartialOrderEReal coverEntropyInf	—	iSup₂_mono' Filter.le_def le_refl
coverEntropyInf_empty 📖	mathematical	—	coverEntropyInf Set Set.instEmptyCollection Bot.bot EReal instBotEReal	—	iSup_congr_Prop coverEntropyInfEntourage_empty iSup_bot
coverEntropyInf_eq_coverEntropy 📖	mathematical	Set.MapsTo	coverEntropyInf coverEntropy	—	le_antisymm coverEntropyInf_le_coverEntropy iSup₂_le comp_symm_mem_uniformity_sets LE.le.trans coverEntropyEntourage_antitone le_iSup₂_of_le coverEntropyEntourage_le_coverEntropyInfEntourage
coverEntropyInf_eq_iSup_basis 📖	mathematical	Filter.HasBasis uniformity	coverEntropyInf iSup EReal instSupSetEReal coverEntropyInfEntourage	—	LE.le.antisymm iSup₂_le Filter.HasBasis.mem_iff LE.le.trans coverEntropyInfEntourage_antitone le_iSup₂ iSup₂_mono' Filter.HasBasis.mem_of_mem le_refl
coverEntropyInf_le_coverEntropy 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal coverEntropyInf coverEntropy	—	iSup₂_mono coverEntropyInfEntourage_le_coverEntropyEntourage
coverEntropyInf_nonneg 📖	mathematical	Set.Nonempty	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal coverEntropyInf	—	LE.le.trans_eq' coverEntropyInfEntourage_le_coverEntropyInf Filter.univ_mem coverEntropyInfEntourage_univ
coverEntropy_antitone 📖	mathematical	—	Antitone UniformSpace EReal PartialOrder.toPreorder instPartialOrderUniformSpace instPartialOrderEReal coverEntropy	—	iSup₂_mono' Filter.le_def le_refl
coverEntropy_empty 📖	mathematical	—	coverEntropy Set Set.instEmptyCollection Bot.bot EReal instBotEReal	—	iSup_congr_Prop coverEntropyEntourage_empty iSup_bot
coverEntropy_eq_iSup_basis 📖	mathematical	Filter.HasBasis uniformity	coverEntropy iSup EReal instSupSetEReal coverEntropyEntourage	—	LE.le.antisymm iSup₂_le Filter.HasBasis.mem_iff LE.le.trans coverEntropyEntourage_antitone le_iSup₂ iSup₂_mono' Filter.HasBasis.mem_of_mem le_refl
coverEntropy_nonneg 📖	mathematical	Set.Nonempty	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal coverEntropy	—	LE.le.trans coverEntropyInf_nonneg coverEntropyInf_le_coverEntropy
coverMincard_antitone 📖	mathematical	—	Antitone SetRel ENat PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat coverMincard	—	biInf_mono IsDynCoverOf.of_entourage_subset
coverMincard_empty 📖	mathematical	—	coverMincard Set Set.instEmptyCollection ENat instZeroENat	—	LE.le.antisymm sInf_le iInf_congr_Prop iInf_pos zero_le
coverMincard_eq_zero_iff 📖	mathematical	—	coverMincard ENat instZeroENat Set Set.instEmptyCollection	—	Finset.coe_empty
coverMincard_finite_iff 📖	mathematical	—	ENat Preorder.toLT PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat coverMincard Top.top instTopENat IsDynCoverOf SetLike.coe Finset Finset.instSetLike ENat.instNatCast Finset.card	—	WithTop.ne_top_iff_exists LT.lt.ne ENat.coe_ne_top ENat.some_eq_coe coverMincard.eq_1 iInf₂_eq_top nonempty_subtype ciInf_mem Set.mem_range iInf_subtype' WithTop.coe_lt_top
coverMincard_finite_of_isCompact_invariant 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace Set.MapsTo SetRel Filter Filter.instMembership uniformity	ENat Preorder.toLT PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat coverMincard Top.top instTopENat	—	exists_isDynCoverOf_of_isCompact_invariant LE.le.trans_lt IsDynCoverOf.coverMincard_le_card WithTop.coe_lt_top
coverMincard_finite_of_isCompact_uniformContinuous 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace UniformContinuous SetRel Filter Filter.instMembership uniformity	ENat Preorder.toLT PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat coverMincard Top.top instTopENat	—	exists_isDynCoverOf_of_isCompact_uniformContinuous LE.le.trans_lt IsDynCoverOf.coverMincard_le_card WithTop.coe_lt_top
coverMincard_le_pow 📖	mathematical	Set.MapsTo	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat coverMincard SetRel.comp Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring instCommSemiringENat	—	LE.le.trans coverMincard_monotone_time LT.lt.le coverMincard_mul_le_pow
coverMincard_monotone_time 📖	mathematical	—	Monotone ENat Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat coverMincard	—	biInf_mono IsDynCoverOf.of_le
coverMincard_mul_le_pow 📖	mathematical	Set.MapsTo	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat coverMincard SetRel.comp Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring instCommSemiringENat	—	Set.eq_empty_or_nonempty coverMincard_empty zero_le eq_or_ne MulZeroClass.mul_zero coverMincard_zero pow_zero le_refl eq_top_or_lt_top ENat.top_pow coverMincard_finite_iff IsDynCoverOf.iterate_le_pow LE.le.trans IsDynCoverOf.coverMincard_le_card WithTop.coe_le_coe
coverMincard_univ 📖	mathematical	Set.Nonempty	coverMincard Set.univ ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	le_antisymm isDynCoverOf_univ Set.singleton_nonempty LE.le.trans_eq IsDynCoverOf.coverMincard_le_card Finset.coe_singleton Finset.card_singleton Nat.cast_one one_le_coverMincard_iff
coverMincard_zero 📖	mathematical	Set.Nonempty	coverMincard ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	le_antisymm isDynCoverOf_zero Set.singleton_nonempty LE.le.trans_eq IsDynCoverOf.coverMincard_le_card Finset.coe_singleton Finset.card_singleton Nat.cast_one one_le_coverMincard_iff
exists_isDynCoverOf_of_isCompact_invariant 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace Set.MapsTo SetRel Filter Filter.instMembership uniformity	IsDynCoverOf SetLike.coe Finset Finset.instSetLike	—	comp_symm_mem_uniformity_sets IsCompact.elim_nhds_subcover UniformSpace.ball_mem_nhds SetRel.IsCover.of_subset_iUnion_ball isSymm_dynEntourage Set.iUnion_congr_Prop dynEntourage_one IsDynCoverOf.iterate_le_pow IsDynCoverOf.of_entourage_subset one_mul
exists_isDynCoverOf_of_isCompact_uniformContinuous 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace UniformContinuous SetRel Filter Filter.instMembership uniformity	IsDynCoverOf SetLike.coe Finset Finset.instSetLike	—	symm_of_uniformity dynEntourage_mem_uniformity IsCompact.elim_nhds_subcover UniformSpace.ball_mem_nhds IsDynCoverOf.of_entourage_subset SetRel.IsCover.of_subset_iUnion_ball isSymm_dynEntourage
isDynCoverOf_empty 📖	mathematical	—	IsDynCoverOf Set Set.instEmptyCollection	—	SetRel.IsCover.empty
isDynCoverOf_empty_right 📖	mathematical	—	IsDynCoverOf Set Set.instEmptyCollection	—	—
isDynCoverOf_univ 📖	mathematical	Set.Nonempty	IsDynCoverOf Set.univ	—	dynEntourage_univ
isDynCoverOf_zero 📖	mathematical	Set.Nonempty	IsDynCoverOf	—	dynEntourage_zero
nonempty_inter_of_coverMincard 📖	mathematical	IsDynCoverOf SetLike.coe Finset Finset.instSetLike ENat ENat.instNatCast Finset.card coverMincard Finset.instMembership	Set.Nonempty Set Set.instInter UniformSpace.ball dynEntourage	—	Mathlib.Tactic.Push.not_forall_eq Finset.coe_erase Finset.mem_coe Set.notMem_empty Set.mem_inter SetRel.symm isSymm_dynEntourage LE.le.not_gt IsDynCoverOf.coverMincard_le_card IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass Finset.card_erase_lt_of_mem
one_le_coverMincard_iff 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat coverMincard Set.Nonempty	—	ENat.one_le_iff_ne_zero Set.nonempty_iff_ne_empty not_iff_not coverMincard_eq_zero_iff

Dynamics.IsDynCoverOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coverEntropyEntourage_le_log_card_div 📖	mathematical	Set.MapsTo Dynamics.IsDynCoverOf SetLike.coe Finset Finset.instSetLike	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal Dynamics.coverEntropyEntourage SetRel.comp DivInvMonoid.toDiv EReal.instDivInvMonoid ENNReal.log ENNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Finset.card instAddCommMonoidWithOneEReal	—	LE.le.trans Dynamics.coverEntropyEntourage_le_log_coverMincard_div EReal.monotone_div_right_of_nonneg Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal ENNReal.log_monotone coverMincard_le_card
coverMincard_le_card 📖	mathematical	Dynamics.IsDynCoverOf SetLike.coe Finset Finset.instSetLike	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat Dynamics.coverMincard ENat.instNatCast Finset.card	—	iInf₂_le
iterate_le_pow 📖	mathematical	Set.MapsTo Dynamics.IsDynCoverOf SetLike.coe Finset Finset.instSetLike	SetRel.comp Finset.card Monoid.toNatPow Nat.instMonoid	—	Set.eq_empty_or_nonempty Finset.coe_empty Nat.instCanonicallyOrderedAdd nonempty MulZeroClass.zero_mul Finset.coe_singleton Finset.card_singleton Dynamics.isDynCoverOf_zero Set.singleton_nonempty one_le_pow_of_one_le' Nat.instMulLeftMono Finset.Nonempty.card_pos Set.empty_subset Set.iInter_congr_Prop Prod.map_iterate UniformSpace.mem_comp_of_mem_ball Function.iterate_add_apply Finset.Nonempty.coe_sort Finset.coe_nonempty Set.MapsTo.iterate SetRel.symm Dynamics.isSymm_dynEntourage Set.toFinset_range Finset.coe_image Finset.coe_univ Set.image_univ SetRel.isSymm_comp_self Set.toFinset_card LE.le.trans Fintype.card_range_le Fintype.card_fun Fintype.card_coe Fintype.card_fin
nonempty 📖	—	Set.Nonempty Dynamics.IsDynCoverOf	—	—	SetRel.IsCover.nonempty
nonempty_inter 📖	mathematical	Dynamics.IsDynCoverOf SetLike.coe Finset Finset.instSetLike	Finset.card Set.Nonempty Set Set.instInter UniformSpace.ball Dynamics.dynEntourage	—	Finset.coe_filter SetRel.symm Dynamics.isSymm_dynEntourage Finset.card_mono Finset.filter_subset
of_entourage_subset 📖	—	SetRel Set.instHasSubset Dynamics.IsDynCoverOf	—	—	SetRel.IsCover.mono_entourage Dynamics.dynEntourage_mono le_refl
of_le 📖	—	Dynamics.IsDynCoverOf	—	—	SetRel.IsCover.mono_entourage Dynamics.dynEntourage_mono subset_refl Set.instReflSubset

---

← Back to Index