eq_fiber_image

Mathlib.Logic.Function.FiberPartition

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

English

The first component of a fiber equals the preimage of its image.

Русский

Первая компонента элемента волокна равна предобразу образа под соответствующей функцией.

LaTeX

$$$a.1 = f^{-1}(\{ a.image \})$$$

Lean4

theorem eq_fiber_image (f : Y → Z) (a : Fiber f) : a.1 = f ⁻¹' { a.image } :=
  a.2.choose_spec.symm

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

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

Разделы

Аффилиация

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