down_surjective

Mathlib.Data.ULift

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

English

The projection down from ULift to the base type is surjective.

Русский

Проекция down из ULift в базовый тип сюръективна.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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