image_inclusion

Mathlib.GroupTheory.GroupAction.SubMulAction

URI: https://scilib.ai/kg/mathlib#SubMulAction.image_inclusion

← MathLib Explorer

English

The range of the inclusion map equals the carrier of p.

Русский

Область определения включения равна носителю p.

LaTeX

$$$ \\mathrm{Set.range}(s.\\mathrm{inclusion}) = s.\\mathrm{carrier} $$$

Lean4

@[to_additive]
theorem image_inclusion (s : SubMulAction M α) : Set.range s.inclusion = s.carrier :=
  by
  rw [inclusion.coe_eq]
  exact Subtype.range_coe

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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