coe_inclusion

Mathlib.Algebra.Group.Subgroup.Defs

URI: https://scilib.ai/kg/mathlib#SubgroupClass.coe_inclusion

English

Composition of the subtype with inclusion equals the subtype of H.

Русский

Компоновка подтипа с включением равна подтипу H.

LaTeX

$$$$ (SubgroupClass.subtype K) \\circ (SubgroupClass.inclusion h) = SubgroupClass.subtype H. $$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_inclusion {H K : S} (h : H ≤ K) (a : H) : (inclusion h a : G) = a :=
  Set.coe_inclusion h a

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

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

Разделы

Аффилиация

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