image_eta

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.image_eta

English

For any set s, the image of s under f equals the image of s under the function x ↦ f(x).

Русский

Для любого множества s образ его под функцией f совпадает с образом множества s под функцией x ↦ f(x).

LaTeX

$$$ f''s = (\\lambda x. f(x))''s $$$

Lean4

theorem image_eta (f : α → β) : f '' s = (fun x => f x) '' s :=
  rfl

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

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

Разделы

Аффилиация

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