mkSelf

Mathlib.Logic.Function.FiberPartition

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

English

The canonical element y is represented by (mk f y).val.

Русский

Канонический элемент y задаётся как значение конструирования волокна mk f y.

LaTeX

$$$(\mathrm{Function.Fiber.mk} \ f \ y).\mathrm{val} = \langle y, rfl \rangle$$$

Lean4

/-- `y : Y` as a term of the type `Fiber.mk f y` -/
def mkSelf (f : Y → Z) (y : Y) : (mk f y).val :=
  ⟨y, rfl⟩

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

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

Разделы

Аффилиация

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