IsInvariant — Mathlib

English

Let ϕ : τ → α → α and s ⊆ α. The set s is invariant under ϕ if for every t ∈ τ, the image ϕ(t)(s) is contained in s.

Русский

Пусть ϕ : τ → α → α и s ⊆ α. Множество s инвариантно относительно ϕ тогда и только тогда, когда для каждого t ∈ τ образ s под действием ϕ(t) содержится в s.

LaTeX

$$$\forall t,\ \varphi(t)[s] \subseteq s$$$

Lean4

/-- A set `s ⊆ α` is invariant under `ϕ : τ → α → α` if `ϕ t s ⊆ s` for all `t` in `τ`. -/
def IsInvariant (ϕ : τ → α → α) (s : Set α) : Prop :=
  ∀ t, MapsTo (ϕ t) s s

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