preimage

Mathlib.Logic.Function.FiberPartition

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

Lean4

/-- An arbitrary element of `a : Fiber f`. -/
noncomputable def preimage (f : Y → Z) (a : Fiber f) : Y :=
  a.2.choose.2.choose

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

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

Разделы

Аффилиация

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