instSetLike — Mathlib

English

The collection of definable sets over A with parameter α is equipped with a SetLike structure, where the underlying set is given by the family of functions α → M and the membership is the usual subset relation.

Русский

Коллекция определяемых множеств над A с параметром α снабжается структурой SetLike: принадлежат они подмножеству функций α → M, а членство определяется как обычное включение подмножеств.

LaTeX

$$$$ \\text{SetLike}((L, A, α)) \\text{ with } (s: L.DefinableSet A α) \\mapsto s \\subseteq (α \\to M). $$$$

Lean4

instance instSetLike : SetLike (L.DefinableSet A α) (α → M)
    where
  coe := Subtype.val
  coe_injective' := Subtype.val_injective

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