map_injective

Mathlib.Data.Finset.Image

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

English

The map f is injective on Finset α: map f is an injection.

Русский

Отображение f инъективно на Finset α: map f — инъекция.

LaTeX

$$$\mathrm{Injective}(\mathrm{map}\ f)$$$

Lean4

theorem map_injective (f : α ↪ β) : Injective (map f) :=
  (mapEmbedding f).injective

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

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

Разделы

Аффилиация

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