g_apply_infinity

Mathlib.Algebra.Category.Grp.EpiMono

URI: https://scilib.ai/kg/mathlib#GrpCat.SurjectiveOfEpiAuxs.g_apply_infinity

English

For every x ∈ B, g(x) fixes the point at infinity: g(x)(∞) = ∞.

Русский

Для любого x ∈ B, g(x) фиксирует точку бесконечности: g(x)(∞) = ∞.

LaTeX

$$$$ g(x)(\infty) = \infty. $$$$

Lean4

theorem g_apply_infinity (x : B) : (g x) ∞ = ∞ :=
  rfl

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

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

Разделы

Аффилиация

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