subtype_comp_rangeRestrict

Mathlib.Algebra.Group.Subgroup.Ker

URI: https://scilib.ai/kg/mathlib#MonoidHom.subtype_comp_rangeRestrict

English

Injectivity of rangeRestrict is equivalent to injectivity of f; i.e. Injective(f.rangeRestrict) ↔ Injective(f).

Русский

Инъективность rangeRestrict эквивалентна инъективности f.

LaTeX

$$Injective(f.rangeRestrict) \Leftrightarrow Injective(f)$$

Lean4

@[to_additive]
theorem subtype_comp_rangeRestrict (f : G →* N) : f.range.subtype.comp f.rangeRestrict = f :=
  ext <| f.coe_rangeRestrict

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

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

Разделы

Аффилиация

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