snd_surjective

Mathlib.Algebra.GroupWithZero.ProdHom

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

English

The second projection snd: G × H → H is surjective.

Русский

Вторая проекция snd: G × H → H сюръективна.

LaTeX

$$$\mathrm{snd}: G_0 \times H_0 \to H_0\quad\text{is surjective, i.e. }\forall h\, \exists g:(g,h)$$$

Lean4

theorem snd_surjective : Function.Surjective (snd G₀ H₀) := by
  classical exact Function.HasRightInverse.surjective ⟨inr .., fun _ ↦ by simp⟩

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

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

Разделы

Аффилиация

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