English
If τ is a canonically ordered additive monoid, then forward invariance and invariance are equivalent: s is forward-invariant under ϕ iff s is invariant under ϕ.
Русский
Если τ — канонически упорядоченный моноид с операцией сложения, то прямая инвариантность и инвариантность эквивалентны: 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 isInvariant [AddMonoid τ] [PartialOrder τ] [CanonicallyOrderedAdd τ] {ϕ : τ → α → α} {s : Set α}
(h : IsForwardInvariant ϕ s) : IsInvariant ϕ s := fun t => h (zero_le t)
