DynamicsEquivalence.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Transport of the metric definition of acylindrical hyperbolicity.

theorem OAI.HarmonicArtin.ParabolicIntersections.AcylindricallyHyperbolic.of_equiv line 11
Source documentation
A group isomorphism transports the action, its uniform acylindricity bounds, and all three distinct orbit limit points.
```
theorem AcylindricallyHyperbolic.of_equiv (e : G ≃* H) (h : AcylindricallyHyperbolic H) :
    AcylindricallyHyperbolic G := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.AcylindricallyHyperbolic