image_eq_preimage

Mathlib.Dynamics.Flow

URI: https://scilib.ai/kg/mathlib#Flow.image_eq_preimage

English

For any t, the image of a set s under ϕ t equals the preimage of s under ϕ (-t).

Русский

Для любого t образ множества s под действием ϕ t равен предобразу s под ϕ(-t).

LaTeX

$$$\\\\varphi t '' s = \\\\varphi(-t)^{-1}' s.$$$

Lean4

theorem image_eq_preimage (t : τ) (s : Set α) : ϕ t '' s = ϕ (-t) ⁻¹' s :=
  (ϕ.toHomeomorph t).toEquiv.image_eq_preimage s

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru