instSetLike — Mathlib

English

The Sylow p-subgroups of a group G carry a natural set-like structure, identified with their underlying subgroups of G via the canonical coe function, and this identification is injective.

Русский

Подпгруппы Силова p группы G образуют естественную структуру множества, которая соответствует их как подгруппам G через естественное встраивание; это соответствие инъективно.

LaTeX

$$$\\mathrm{SetLike}(Sylow_p(G), G)$$$

Lean4

instance : SetLike (Sylow p G) G where
  coe := (↑)
  coe_injective' _ _ h := ext (SetLike.coe_injective h)

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