IsForwardInvariant — Mathlib

English

A set s is forward-invariant under ϕ if ϕ(t)(s) ⊆ s for all t ≥ 0.

Русский

Множество s является прямой (форвард) инвариантностью относительно ϕ, если для всех t ≥ 0 выполняется ϕ(t)(s) ⊆ s.

LaTeX

$$$\forall t\, (0 \le t) \;\Rightarrow\; ϕ(t)[s] \subseteq s$$$

Lean4

/-- A set `s ⊆ α` is forward-invariant under `ϕ : τ → α → α` if `ϕ t s ⊆ s` for all `t ≥ 0`. -/
def IsForwardInvariant [Preorder τ] [Zero τ] (ϕ : τ → α → α) (s : Set α) : Prop :=
  ∀ ⦃t⦄, 0 ≤ t → MapsTo (ϕ t) s s

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