instSetLike — Mathlib

English

There is a canonical way to regard OpenNormalSubgroup G as a subset of G, via its underlying set of elements, and equality is detected by equality of these underlying sets.

Русский

Существует канонический способ рассматривать OpenNormalSubgroup G как подмножество G через множество элементов, и равенство подгрупп определяется равенством их множества элементов.

LaTeX

$$instSetLike: OpenNormalSubgroup(G) is SetLike(G) with coe(H) = H.1$$

Lean4

@[to_additive]
instance : SetLike (OpenNormalSubgroup G) G where
  coe U := U.1
  coe_injective' _ _ h := toSubgroup_injective <| SetLike.ext' h

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