instCoeTCElem

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#instCoeTCElem

English

There is a natural inclusion map from a subset s ⊆ α into α, sending x ∈ s to x from α.

Русский

Существует естественное вложение элементов подмножества s ⊆ α в α, отображающее x ∈ s в x из α.

LaTeX

$$$\\iota: s \\to \\alpha,\\quad \\iota(\\langle a, h \\rangle) = a$$$

Lean4

instance (s : Set α) : CoeTC s α :=
  ⟨fun x => x.1⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru