isForwardInvariant_iff_isInvariant

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⟩

Похожие утверждения