map_eq_image

Mathlib.Data.Finset.Image

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

English

For an embedding f: α ↪ β, s.map f equals s.image f.

Русский

Для вложения f: α ↪ β отображение s.map f равно s.image f.

LaTeX

$$$s\\mapsto f = s.image f$$$

Lean4

theorem map_eq_image (f : α ↪ β) (s : Finset α) : s.map f = s.image f :=
  eq_of_veq (s.map f).2.dedup.symm

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

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

Разделы

Аффилиация

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