down_surjective

Mathlib.Data.ULift

URI: https://scilib.ai/kg/mathlib#PLift.down_surjective

English

The projection down: PLift α → α is surjective.

Русский

Проекция down: PLift α → α сюръективна.

LaTeX

$$$\\forall a \\in \\alpha, \\exists x \\in \\mathrm{PLift}(\\alpha), \\mathrm{down}(x) = a$$$

Lean4

theorem down_surjective : Surjective (@down α) :=
  Equiv.plift.surjective

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

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

Разделы

Аффилиация

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