types_π_surjective

Mathlib.CategoryTheory.GlueData

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GlueData.types_π_surjective

English

The function π from the multispan to the glued types is surjective.

Русский

Функция π из мульти-спана на склеенные типы сюръективна.

LaTeX

$$$\\operatorname{Surjective}(\\pi)$$$

Lean4

theorem types_π_surjective (D : GlueData Type*) : Function.Surjective D.π :=
  (epi_iff_surjective _).mp inferInstance

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

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

Разделы

Аффилиация

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