fst_surjective

Mathlib.Algebra.GroupWithZero.ProdHom

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

English

The first projection fst: G × H → G is surjective.

Русский

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

LaTeX

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

Lean4

theorem fst_surjective : Function.Surjective (fst G₀ H₀) := by
  classical exact Function.HasRightInverse.surjective ⟨inl .., fun _ ↦ by simp⟩

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

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

Разделы

Аффилиация

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