isForwardInvariant — Mathlib

English

If s is invariant under ϕ, then s is forward-invariant under ϕ.

Русский

Если множество s инвариантно относительно ϕ, то оно является прямой инвариантностью относительно ϕ.

LaTeX

$$$\operatorname{IsInvariant}(\varphi, s) \Rightarrow \operatorname{IsForwardInvariant}(\varphi, s)$$$

Lean4

theorem isForwardInvariant [Preorder τ] [Zero τ] {ϕ : τ → α → α} {s : Set α} (h : IsInvariant ϕ s) :
    IsForwardInvariant ϕ s := fun t _ht => h t

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