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]