Documentation Verification Report

DynamicalEntourage

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

Statistics

Metric	Count
Definitions `dynEntourage`	1
Theorems `ball_dynEntourage_mem_nhds`, `dynEntourage_antitone`, `dynEntourage_comp_subset`, `dynEntourage_eq_inter_Ico`, `dynEntourage_mem_uniformity`, `dynEntourage_mono`, `dynEntourage_monotone`, `dynEntourage_one`, `dynEntourage_univ`, `dynEntourage_zero`, `idRel_subset_dynEntourage`, `isRefl_dynEntourage`, `isSymm_dynEntourage`, `mem_ball_dynEntourage`, `mem_ball_dynEntourage_comp`, `mem_dynEntourage`, `preimage_dynEntourage`, `dynEntourage`, `dynEntourage`	19
Total	20

Dynamics

Definitions

Name	Category	Theorems
`dynEntourage` 📖	CompOp	20 math math: `isSymm_dynEntourage`, `ball_dynEntourage_mem_nhds`, `nonempty_inter_of_coverMincard`, `idRel_subset_dynEntourage`, `IsDynCoverOf.nonempty_inter`, `isOpen.dynEntourage`, `mem_dynEntourage`, `dynEntourage_comp_subset`, `dynEntourage_mem_uniformity`, `dynEntourage_one`, `dynEntourage_mono`, `isRefl_dynEntourage`, `dynEntourage_zero`, `dynEntourage_univ`, `dynEntourage_antitone`, `mem_ball_dynEntourage`, `Function.Semiconj.preimage_dynEntourage`, `IsSymmetricRel.dynEntourage`, `dynEntourage_eq_inter_Ico`, `dynEntourage_monotone`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_dynEntourage_mem_nhds` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `SetRel` `Filter` `Filter.instMembership` `uniformity`	`Set` `nhds` `UniformSpace.ball` `dynEntourage`	—	`dynEntourage_eq_inter_Ico` `UniformSpace.ball_iInter` `Filter.iInter_mem` `Finite.of_fintype` `Prod.map_iterate` `ball_preimage` `ContinuousAt.preimage_mem_nhds` `Continuous.continuousAt` `Continuous.iterate` `UniformSpace.ball_mem_nhds`
`dynEntourage_antitone` 📖	mathematical	—	`Antitone` `SetRel` `Nat.instPreorder` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `dynEntourage`	—	`Set.iInter₂_mono'` `lt_of_lt_of_le` `subset_refl` `Set.instReflSubset`
`dynEntourage_comp_subset` 📖	mathematical	—	`SetRel` `Set.instHasSubset` `SetRel.comp` `dynEntourage`	—	`Set.iInter_congr_Prop` `Prod.map_iterate` `UniformSpace.mem_ball_comp`
`dynEntourage_eq_inter_Ico` 📖	mathematical	—	`dynEntourage` `Set.iInter` `Set.Elem` `Set.Ico` `Nat.instPreorder` `Set.preimage` `Nat.iterate` `Set` `Set.instMembership`	—	`Set.iInter_congr_Prop` `Prod.map_iterate` `Set.iInter_coe_set`
`dynEntourage_mem_uniformity` 📖	mathematical	`UniformContinuous` `SetRel` `Filter` `Filter.instMembership` `uniformity`	`dynEntourage`	—	`dynEntourage_eq_inter_Ico` `Prod.map_iterate` `Set.iInter_of_empty` `Set.Ico_eq_empty` `Set.iInter_coe_set` `Set.iInter_congr_Prop` `Set.biInter_lt_succ` `Filter.inter_mem` `uniformContinuous_def` `UniformContinuous.iterate`
`dynEntourage_mono` 📖	mathematical	`SetRel` `Set.instHasSubset`	`dynEntourage`	—	`LE.le.trans` `dynEntourage_monotone` `dynEntourage_antitone`
`dynEntourage_monotone` 📖	mathematical	—	`Monotone` `SetRel` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `dynEntourage`	—	`Set.iInter₂_mono` `Set.preimage_mono`
`dynEntourage_one` 📖	mathematical	—	`dynEntourage`	—	`Set.iInter_congr_Prop` `Prod.map_iterate` `Set.iInter_iInter_eq_left`
`dynEntourage_univ` 📖	mathematical	—	`dynEntourage` `Set.univ`	—	`Set.iInter_congr_Prop` `Prod.map_iterate` `Set.iInter_univ`
`dynEntourage_zero` 📖	mathematical	—	`dynEntourage` `Set.univ`	—	`Set.iInter_congr_Prop` `Prod.map_iterate` `Set.iInter_of_empty` `instIsEmptyFalse` `Set.iInter_univ`
`idRel_subset_dynEntourage` 📖	mathematical	`Set` `Set.instHasSubset` `idRel`	`dynEntourage`	—	`Set.iInter_congr_Prop` `Prod.map_iterate`
`isRefl_dynEntourage` 📖	mathematical	—	`SetRel.IsRefl` `dynEntourage`	—	`Set.iInter_congr_Prop` `Prod.map_iterate` `SetRel.isRefl_iInter` `SetRel.isRefl_preimage`
`isSymm_dynEntourage` 📖	mathematical	—	`SetRel.IsSymm` `dynEntourage`	—	`Set.iInter_congr_Prop` `Prod.map_iterate` `SetRel.isSymm_iInter` `SetRel.isSymm_preimage`
`mem_ball_dynEntourage` 📖	mathematical	—	`Set` `Set.instMembership` `UniformSpace.ball` `dynEntourage` `Nat.iterate`	—	—
`mem_ball_dynEntourage_comp` 📖	mathematical	`Set.Nonempty` `Set` `Set.instInter` `UniformSpace.ball` `dynEntourage`	`Set.instMembership` `SetRel.comp`	—	`dynEntourage_comp_subset` `UniformSpace.mem_ball_comp` `UniformSpace.mem_ball_symmetry` `isSymm_dynEntourage`
`mem_dynEntourage` 📖	mathematical	—	`SetRel` `Set.instMembership` `dynEntourage` `Nat.iterate`	—	`Set.iInter_congr_Prop` `Prod.map_iterate`

Function.Semiconj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_dynEntourage` 📖	mathematical	`Function.Semiconj`	`Set.preimage` `Dynamics.dynEntourage`	—	`Dynamics.dynEntourage.eq_1` `Set.preimage_iInter₂` `Set.iInter₂_congr` `Set.preimage_comp` `Prod.map_iterate` `comp_eq` `iterate_right`

IsSymmetricRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dynEntourage` 📖	mathematical	`IsSymmetricRel`	`Dynamics.dynEntourage`	—	`Set.ext` `Set.iInter_congr_Prop` `Prod.map_iterate` `mk_mem_comm` `Prod.map_apply'`

isOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dynEntourage` 📖	mathematical	`Continuous` `IsOpen` `instTopologicalSpaceProd`	`Dynamics.dynEntourage`	—	`Dynamics.dynEntourage_eq_inter_Ico` `isOpen_iInter_of_finite` `Finite.of_fintype` `IsOpen.preimage` `Continuous.iterate` `Continuous.prodMap`

---

← Back to Index