isInvariant_iff_image_eq — Mathlib

English

For a flow ϕ on α, IsInvariant ϕ s is equivalent to the condition that for all t, the image of s under ϕ t is s.

Русский

Для потока ϕ на α инвариантность множества s эквивалентна тому, что для каждого t множество-образ s под ϕ t равно самому s.

LaTeX

$$$IsInvariant\\\\ ϕ\\\\ s \\iff \\\\forall t,\\\\ ϕ t '' s = s.$$$

Lean4

theorem isInvariant_iff_image_eq (s : Set α) : IsInvariant ϕ s ↔ ∀ t, ϕ t '' s = s :=
  (isInvariant_iff_image _ _).trans
    (Iff.intro (fun h t => Subset.antisymm (h t) fun _ hx => ⟨_, h (-t) ⟨_, hx, rfl⟩, by simp [← map_add]⟩) fun h t =>
      by rw [h t])

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