instSetLike — Mathlib

English

There is a SetLike structure on Subgroup G given by the carrier map s ↦ s.carrier.

Русский

Существует структура SetLike на Subgroup G, заданная отображением носителя s ↦ s.carrier.

LaTeX

$$$$ \\text{Subgroup instSetLike: SetLike }(\\mathrm{Subgroup} G) G \\text{ with } \\mathrm{coe}(s)=s.\\text{carrier}. $$$$

Lean4

@[to_additive]
instance : SetLike (Subgroup G) G where
  coe s := s.carrier
  coe_injective' p q
    h := by
    obtain ⟨⟨⟨hp, _⟩, _⟩, _⟩ := p
    obtain ⟨⟨⟨hq, _⟩, _⟩, _⟩ := q
    congr

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