snd_surjective

Mathlib.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.snd_surjective

English

The second projection from TrivSqZeroExt R M to M is surjective when M is a nonempty set and R is nonempty.

Русский

Вторая проекция из TrivSqZeroExt R M на M сюръективна при определённых условиях на R и M.

LaTeX

$$snd : tsze R M → M является сюръективной$$

Lean4

theorem snd_surjective [Nonempty R] : Function.Surjective (snd : tsze R M → M) :=
  Prod.snd_surjective

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

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

Разделы

Аффилиация

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