map_preimage_eq_image

Mathlib.Logic.Function.FiberPartition

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

English

For a fiber a of g ∘ f, g(f(a.preimage)) equals a.image.

Русский

Для волокна a от композиции g ∘ f выполняется g( f(a.preimage) ) = a.image.

LaTeX

$$$g (f a.preimage) = a.image$$$

Lean4

theorem map_preimage_eq_image (f : Y → Z) (a : Fiber f) : f a.preimage = a.image :=
  a.2.choose.2.choose_spec

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

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

Разделы

Аффилиация

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