instCoeSortType — Mathlib

English

There is a canonical coercion from the set of α to the type of its elements, given by s ↦ Elem(s).

Русский

Существует каноническое вложение из множества s ⊆ α в тип элементов s, заданное отображением s ↦ Elem(s).

LaTeX

$$$\text{There exists a canonical coercion } \mathrm{Set}(\alpha) \to \mathrm{Type}$, $s \mapsto \mathrm{Elem}(s)$.$$

Lean4

/-- Coercion from a set to the corresponding subtype. -/
instance : CoeSort (Set α) (Type u) :=
  ⟨Elem⟩

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