image_snd_graphOn

Mathlib.Data.Set.Prod

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

English

The second-coordinate projection of the graph of f on s is the image f[s].

Русский

Проекция по второй координате графа f на s равна изображению f[s].

LaTeX

$$$\operatorname{image} \operatorname{snd} (\operatorname{graphOn}(f,s)) = f''s$$$

Lean4

@[simp]
theorem image_snd_graphOn (f : α → β) : Prod.snd '' s.graphOn f = f '' s := by ext x; simp

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

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

Разделы

Аффилиация

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