isInvariant_iff_image — Mathlib

English

A set s is invariant under ϕ if and only if for every t, the image of s under ϕ(t) is contained in s.

Русский

Множество s инвариантно относительно ϕ тогда и только тогда, когда для каждого t образ s под действием ϕ(t) содержится в s.

LaTeX

$$$\operatorname{IsInvariant}(\varphi, s) \iff \forall t,\ \varphi(t)[s] \subseteq s$$$

Lean4

theorem isInvariant_iff_image : IsInvariant ϕ s ↔ ∀ t, ϕ t '' s ⊆ s := by simp_rw [IsInvariant, mapsTo_iff_image_subset]

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