image_singleton

Mathlib.Data.Set.Image

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

English

The image of a singleton under f is a singleton: f''{a} = {f(a)}.

Русский

Образ множества-одиночки под действием f —也是 одиночка: f''{a} = {f(a)}.

LaTeX

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

Lean4

@[simp]
theorem image_singleton {f : α → β} {a : α} : f '' { a } = {f a} := by grind

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

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

Разделы

Аффилиация

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