coe_injective

Mathlib.Data.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.coe_injective

English

The map s ↦ (s : Set α) from Finset α to Set α is injective.

Русский

Отображение Finset α в Set α по выражению s ↦ (s : Set α) инъективно.

LaTeX

$$$ \text{Injective}((\uparrow) : \mathrm{Finset} \alpha \to \mathrm{Set} \alpha)$$$

Lean4

theorem coe_injective {α} : Injective ((↑) : Finset α → Set α) := fun _s _t => coe_inj.1

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

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

Разделы

Аффилиация

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