π_surjective — Mathlib

English

The glue projection π is surjective; every point in the glued space comes from some piece.

Русский

Отображение π из сцепления распространяется по всей слитой пространстве; каждый элемент берётся из одной из частей.

LaTeX

$$$\text{π is surjective}$$$

Lean4

theorem π_surjective : Function.Surjective 𝖣.π :=
  (TopCat.epi_iff_surjective 𝖣.π).mp inferInstance

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