English
Under canonical ordered additive monoid assumptions, IsForwardInvariant ϕ s is equivalent to IsInvariant ϕ s.
Русский
При предположениях о канонически упорядоченном моноиде равносильны IsForwardInvariant ϕ s и IsInvariant ϕ s.
LaTeX
$$$\operatorname{IsForwardInvariant}(\varphi, s) \iff \operatorname{IsInvariant}(\varphi, s)$$$
Lean4
/-- If `τ` is a `CanonicallyOrderedAdd` monoid (e.g., `ℕ` or `ℝ≥0`), then the notions
`IsForwardInvariant` and `IsInvariant` are equivalent. -/
theorem isForwardInvariant_iff_isInvariant [AddMonoid τ] [PartialOrder τ] [CanonicallyOrderedAdd τ] {ϕ : τ → α → α}
{s : Set α} : IsForwardInvariant ϕ s ↔ IsInvariant ϕ s :=
⟨IsForwardInvariant.isInvariant, IsInvariant.isForwardInvariant⟩