sigmaIncl

Mathlib.Topology.FiberPartition

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Fiber.sigmaIncl

← MathLib Explorer

English

The inclusion map from a fiber a of f into S is given by sending x to x.val.

Русский

Включение из Fibre a функции f в S отправляет x на x.val.

LaTeX

$$$$\sigma\text{Incl}_{f}(a):\; a.\mathrm{val} \to S,\quad \sigma\text{Incl}_{f}(a)(x)=x.\mathrm{val}.$$$$

Lean4

/-- The inclusion map from a component of the disjoint union induced by `f` into `S`. -/
def sigmaIncl (a : Fiber f) : C(a.val, S) where toFun x := x.val

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

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

Разделы

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

Аффилиация

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