map_refl

Mathlib.Data.Finset.Image

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

English

Let s be a Finset of α. The image of s under the identity embedding α ↪ α is s itself.

Русский

Пусть s — Finset α. Образ этого множества при тождественном отображении α → α равен самому s.

LaTeX

$$$s.map(\\mathrm{Embedding.refl}\\alpha) = s$$$

Lean4

@[simp]
theorem map_refl : s.map (Embedding.refl _) = s :=
  ext fun _ => by simpa only [mem_map, exists_prop] using exists_eq_right

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

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

Разделы

Аффилиация

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