mk_image

Mathlib.Logic.Function.FiberPartition

URI: https://scilib.ai/kg/mathlib#Function.Fiber.mk_image

English

The image of Fiber.mk f y is f y.

Русский

Образ волокна Fiber.mk f y равен f y.

LaTeX

$$$(\mathrm{Fiber.mk} f y).\mathrm{image} = f y$$$

Lean4

theorem mk_image (f : Y → Z) (y : Y) : (Fiber.mk f y).image = f y :=
  (map_eq_image (x := mkSelf f y)).symm

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

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

Разделы

Аффилиация

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