mk

Mathlib.Logic.Function.FiberPartition

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

Lean4

/-- Given `y : Y`, `Fiber.mk f y` is the fiber of `f` that `y` belongs to, as an element of `Fiber f`.
-/
def mk (f : Y → Z) (y : Y) : Fiber f :=
  ⟨f ⁻¹' {f y}, by simp⟩

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

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

Разделы

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

Аффилиация

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