range_swap

Mathlib.GroupTheory.Coprod.Basic

URI: https://scilib.ai/kg/mathlib#Monoid.Coprod.range_swap

English

The image of the swap map on the coproduct has full range (equals top).

Русский

Образ отображения swap на копродукт имеет полное множество значений.

LaTeX

$$$\operatorname{range}(\mathrm{swap}\, G\, H) = \top.$$$

Lean4

@[to_additive (attr := simp)]
theorem range_swap : MonoidHom.range (swap G H) = ⊤ :=
  MonoidHom.range_eq_top.2 swap_surjective

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

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

Разделы

Аффилиация

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