preimage_inv

Mathlib.GroupTheory.Perm.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.preimage_inv

English

For a bijection f, the preimage of a set s under f^{-1} equals the image of s under f: f^{-1}[s] = f[s].

Русский

Для биекции f прообраз по f^{-1} множества s совпадает с образцом множества s по f: f^{-1}[s] = f[s].

LaTeX

$$$f^{-1}[s] = f[s].$$$

Lean4

@[simp]
theorem preimage_inv (f : Perm α) (s : Set α) : ↑f⁻¹ ⁻¹' s = f '' s :=
  (f.image_eq_preimage _).symm

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

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

Разделы

Аффилиация

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