mapEmbedding_apply

Mathlib.Data.Finset.Image

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

English

The mapEmbedding is equal to the map when applied to a Finset: mapEmbedding f s = map f s.

Русский

MapEmbedding совпадает с map при применении к Finset: mapEmbedding f s = map f s.

LaTeX

$$$mapEmbedding f\, s = map f\, s$$$

Lean4

@[simp]
theorem mapEmbedding_apply : mapEmbedding f s = map f s :=
  rfl

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

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

Разделы

Аффилиация

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