image_id'

Mathlib.Data.Finset.Image

URI: https://scilib.ai/kg/mathlib#Finset.image_id'

English

Let s be a finite set of α. The image of s under the identity map is s; i.e., image id s = s.

Русский

Пусть s — конечное множество в α. Образ под тождественным отображением равен s, то есть image id s = s.

LaTeX

$$$\mathrm{image}\ \mathrm{id}\ s = s$$$

Lean4

@[simp]
theorem image_id' [DecidableEq α] : (s.image fun x => x) = s :=
  image_id

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

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

Разделы

Аффилиация

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