instSetLike — Mathlib

English

ClosedSubgroup is a SetLike structure over G, with coe and coercion properties.

Русский

ClosedSubgroup образует структуру SetLike над G с отображением включения и связанными свойствами наличие коe.

LaTeX

$$$ \\text{SetLike}(\\text{ClosedSubgroup } G) \\quad$$$

Lean4

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

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