Mathlib Map

Theorems · Theorem · dynamical systems

Dynamics.IsDynNetIn.of_le

∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {m n : ℕ} {F s : Set X},
  m ≤ n → Dynamics.IsDynNetIn T F U m s → Dynamics.IsDynNetIn T F U n s
Defined in
Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Cited by
1 results in Mathlib
Foundations
Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Dynamics.netMaxcard_monotone_time · cited by 1Dynamics.netMaxcard_monot…Set · cited by 53352SetSetRel · cited by 581SetRelUniformSpace.ball_mono · cited by 20UniformSpace.ball_monoDynamics.IsDynNetIn · cited by 18Dynamics.IsDynNetInSet.PairwiseDisjoint.mono · cited by 8PairwiseDisjoint.monoDynamics.dynEntourage_antitone · cited by 2Dynamics.dynEntourage_ant…IsDynNetIn.of_leCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.