instSetLike — Mathlib

English

A subring structure provides a SetLike structure on Subring R, i.e., its carrier is a subset of R with a membership predicate.

Русский

Структура подкольца задаёт SetLike-структуру для Subring R: носитель — подмножество R с гомогенным членством.

LaTeX

$$$ \\text{SetLike}(\\mathrm{Subring}(R), R) $$$

Lean4

instance : SetLike (Subring R) R where
  coe s := s.carrier
  coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h

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