Fiber

Mathlib.Logic.Function.FiberPartition

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

Lean4

/-- The indexing set of the partition. -/
def Fiber (f : Y → Z) : Type _ :=
  Set.range (fun (x : Set.range f) ↦ f ⁻¹' { x.val })

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

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

Разделы

Аффилиация

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