image_pair

Mathlib.Data.Set.Image

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

English

The image of a two-point set {a,b} is the two-point set {f(a), f(b)}.

Русский

Образ множества из двух элементов {a,b} равен {f(a), f(b)}.

LaTeX

$$$ f''\\{a,b\\} = \\{f(a), f(b)\\}. $$$

Lean4

theorem image_pair (f : α → β) (a b : α) : f '' { a, b } = {f a, f b} := by grind

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

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

Разделы

Аффилиация

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