subtype_comp_inclusion — Mathlib

English

Composition of the subtype with inclusion equals the subtype of H (variant statement).

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem subtype_comp_inclusion {H K : S} (h : H ≤ K) :
    (SubgroupClass.subtype K).comp (inclusion h) = SubgroupClass.subtype H :=
  rfl

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