fmap_def

Mathlib.Data.Finset.Functor

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

English

For any function f : α → β, the Finset Functor map f applied to s is equal to the Finset image of f on s.

Русский

Для любой функции f : α → β отображение Finset через f совпадает с образом Finset через f на s.

LaTeX

$$$$ f \\<\\!> s = s.IMAGE f $$$$

Lean4

@[simp]
theorem fmap_def {s : Finset α} (f : α → β) : f <$> s = s.image f :=
  rfl

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

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

Разделы

Аффилиация

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