Documentation Verification Report

Semiconj

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

Statistics

Metric	Count
Definitions `Semiconj`	1
Theorems `image`, `preimage`, `coverEntropyEntourage_image_le`, `coverEntropyInfEntourage_image_le`, `coverEntropyInf_image_le_of_uniformContinuous`, `coverEntropyInf_image_le_of_uniformContinuousOn_invariant`, `coverEntropyInf_image_of_comap`, `coverEntropyInf_restrict_subset`, `coverEntropy_image_le_of_uniformContinuous`, `coverEntropy_image_le_of_uniformContinuousOn_invariant`, `coverEntropy_image_of_comap`, `coverEntropy_restrict`, `coverEntropy_restrict_subset`, `coverMincard_image_le`, `le_coverEntropyEntourage_image`, `le_coverEntropyInfEntourage_image`, `le_coverMincard_image`	17
Total	18

Dynamics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coverEntropyEntourage_image_le` 📖	mathematical	`Function.Semiconj`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `coverEntropyEntourage` `Set.image` `Set.preimage`	—	`ExpGrowth.expGrowthSup_monotone` `ENat.toENNReal_mono` `coverMincard_image_le`
`coverEntropyInfEntourage_image_le` 📖	mathematical	`Function.Semiconj`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `coverEntropyInfEntourage` `Set.image` `Set.preimage`	—	`ExpGrowth.expGrowthInf_monotone` `ENat.toENNReal_mono` `coverMincard_image_le`
`coverEntropyInf_image_le_of_uniformContinuous` 📖	mathematical	`Function.Semiconj` `UniformContinuous`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `coverEntropyInf` `Set.image`	—	`coverEntropyInf_image_of_comap` `coverEntropyInf_antitone` `uniformContinuous_iff`
`coverEntropyInf_image_le_of_uniformContinuousOn_invariant` 📖	mathematical	`Function.Semiconj` `UniformContinuousOn` `Set` `Set.instHasSubset` `Set.MapsTo`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `coverEntropyInf` `Set.image`	—	`coverEntropyInf_restrict_subset` `Set.restrict_apply` `Set.MapsTo.val_restrict_apply` `Function.Semiconj.eq` `LE.le.trans_eq'` `coverEntropyInf_image_le_of_uniformContinuous` `uniformContinuousOn_iff_restrict` `Set.image_image_val_eq_restrict_image` `Subtype.image_preimage_coe` `Set.inter_eq_right`
`coverEntropyInf_image_of_comap` 📖	mathematical	`Function.Semiconj`	`coverEntropyInf` `Set.image` `UniformSpace.comap`	—	`le_antisymm` `iSup₂_le` `LE.le.trans` `coverEntropyInfEntourage_antitone` `SetRel.symmetrize_subset_self` `coverEntropyInfEntourage_image_le` `coverEntropyInfEntourage_le_coverEntropyInf` `uniformity_comap` `Filter.mem_comap` `symmetrize_mem_uniformity` `Set.Subset.rfl` `comp_symm_mem_uniformity_sets` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.preimage_mono` `le_coverEntropyInfEntourage_image`
`coverEntropyInf_restrict_subset` 📖	mathematical	`Set` `Set.instHasSubset` `Set.MapsTo`	`coverEntropyInf` `Set.Elem` `instUniformSpaceSubtype` `Set.instMembership` `Set.MapsTo.restrict` `Set.preimage`	—	`coverEntropyInf_image_of_comap` `Set.MapsTo.val_restrict_apply` `Subtype.image_preimage_coe` `Set.inter_eq_right`
`coverEntropy_image_le_of_uniformContinuous` 📖	mathematical	`Function.Semiconj` `UniformContinuous`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `coverEntropy` `Set.image`	—	`coverEntropy_image_of_comap` `coverEntropy_antitone` `uniformContinuous_iff`
`coverEntropy_image_le_of_uniformContinuousOn_invariant` 📖	mathematical	`Function.Semiconj` `UniformContinuousOn` `Set` `Set.instHasSubset` `Set.MapsTo`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `coverEntropy` `Set.image`	—	`coverEntropy_restrict_subset` `Set.restrict_apply` `Set.MapsTo.val_restrict_apply` `Function.Semiconj.eq` `LE.le.trans_eq'` `coverEntropy_image_le_of_uniformContinuous` `uniformContinuousOn_iff_restrict` `Set.image_image_val_eq_restrict_image` `Subtype.image_preimage_coe` `Set.inter_eq_right`
`coverEntropy_image_of_comap` 📖	mathematical	`Function.Semiconj`	`coverEntropy` `Set.image` `UniformSpace.comap`	—	`le_antisymm` `iSup₂_le` `LE.le.trans` `coverEntropyEntourage_antitone` `SetRel.symmetrize_subset_self` `coverEntropyEntourage_image_le` `coverEntropyEntourage_le_coverEntropy` `uniformity_comap` `Filter.mem_comap` `symmetrize_mem_uniformity` `Set.Subset.rfl` `comp_symm_mem_uniformity_sets` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.preimage_mono` `le_coverEntropyEntourage_image`
`coverEntropy_restrict` 📖	mathematical	`Set.MapsTo`	`coverEntropy` `Set.Elem` `instUniformSpaceSubtype` `Set` `Set.instMembership` `Set.MapsTo.restrict` `Set.univ`	—	`coverEntropy_restrict_subset` `Set.Subset.rfl` `Subtype.coe_preimage_self`
`coverEntropy_restrict_subset` 📖	mathematical	`Set` `Set.instHasSubset` `Set.MapsTo`	`coverEntropy` `Set.Elem` `instUniformSpaceSubtype` `Set.instMembership` `Set.MapsTo.restrict` `Set.preimage`	—	`coverEntropy_image_of_comap` `Set.MapsTo.val_restrict_apply` `Subtype.image_preimage_coe` `Set.inter_eq_right`
`coverMincard_image_le` 📖	mathematical	`Function.Semiconj`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `coverMincard` `Set.image` `Set.preimage`	—	`eq_top_or_lt_top` `le_top` `coverMincard_finite_iff` `IsDynCoverOf.image` `LE.le.trans` `IsDynCoverOf.coverMincard_le_card` `Finset.coe_image` `WithTop.coe_le_coe` `Finset.card_image_le`
`le_coverEntropyEntourage_image` 📖	mathematical	`Function.Semiconj`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `coverEntropyEntourage` `Set.preimage` `SetRel.comp` `Set.image`	—	`ExpGrowth.expGrowthSup_monotone` `ENat.toENNReal_mono` `le_coverMincard_image`
`le_coverEntropyInfEntourage_image` 📖	mathematical	`Function.Semiconj`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `coverEntropyInfEntourage` `Set.preimage` `SetRel.comp` `Set.image`	—	`ExpGrowth.expGrowthInf_monotone` `ENat.toENNReal_mono` `le_coverMincard_image`
`le_coverMincard_image` 📖	mathematical	`Function.Semiconj`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `coverMincard` `Set.preimage` `SetRel.comp` `Set.image`	—	`eq_top_or_lt_top` `le_top` `coverMincard_finite_iff` `IsDynCoverOf.preimage` `LE.le.trans` `IsDynCoverOf.coverMincard_le_card` `WithTop.coe_le_coe`

Dynamics.IsDynCoverOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image` 📖	mathematical	`Function.Semiconj` `Dynamics.IsDynCoverOf` `Set.preimage`	`Set.image`	—	`Set.mem_image_of_mem` `Function.Semiconj.preimage_dynEntourage`
`preimage` 📖	mathematical	`Function.Semiconj` `Dynamics.IsDynCoverOf` `Set.image` `SetLike.coe` `Finset` `Finset.instSetLike`	`Set.preimage` `SetRel.comp` `Finset.card`	—	`isEmpty_or_nonempty` `Dynamics.isDynCoverOf_empty` `zero_le` `Nat.instCanonicallyOrderedAdd` `Finset.card_empty` `Set.eq_empty_of_isEmpty` `instIsEmptySubtype` `nonempty_inter` `Finset.coe_image` `Set.image_congr` `Function.Semiconj.preimage_dynEntourage` `Set.mem_image_of_mem` `Dynamics.dynEntourage_comp_subset` `LE.le.trans` `Finset.card_image_le` `Function.sometimes_spec` `Set.nonempty_def`

Function

Definitions

Name	Category	Theorems
`Semiconj` 📖	MathDef	20 math math: `csSup_div_semiconj`, `AddSemiconjBy.function_semiconj_add_right_swap`, `Flow.IsSemiconjugacy.semiconj`, `Equiv.semiconj_conj`, `sSup_div_semiconj`, `AddConstMapClass.semiconj`, `Semiconj.swap_map`, `Semiconj.id_right`, `CircleDeg1Lift.semiconj_of_isUnit_of_translationNumber_eq`, `SemiconjBy.function_semiconj_mul_right_swap`, `CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq`, `Semiconj.id_left`, `SemiconjBy.function_semiconj_mul_left`, `semiconj_of_isLUB`, `AddSemiconjBy.function_semiconj_add_left`, `CircleDeg1Lift.units_semiconj_of_translationNumber_eq`, `CircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq`, `Commute.semiconj`, `semiconj_iff_comp_eq`, `CircleDeg1Lift.semiconjBy_iff_semiconj`

---

← Back to Index