image

Mathlib.Logic.Function.FiberPartition

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

Lean4

/-- Any `a : Fiber f` is of the form `f ⁻¹' {x}` for some `x` in the image of `f`. We define `a.image`
as an arbitrary such `x`.
-/
noncomputable def image (f : Y → Z) (a : Fiber f) : Z :=
  a.2.choose.1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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