setLike — Mathlib

English

There is a SetLike structure on Submodule R M, i.e., Submodule R M can be viewed as a collection of elements of M with a compatible membership predicate.

Русский

Для подполя Submodule R M существует структура SetLike, которая позволяет рассматривать подмодуль как множество элементов M с совместимым членством.

LaTeX

$$$\\text{SetLike} (\\text{Submodule}(R,M))$$$

Lean4

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

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