image_empty

Mathlib.Data.Finset.Image

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

English

The image of the empty Finset under any function is empty.

Русский

Образ пустого финсетa под любым отображением есть пустота.

LaTeX

$$$\\operatorname{image}(f, \\emptyset) = \\emptyset$$$

Lean4

@[simp]
theorem image_empty (f : α → β) : (∅ : Finset α).image f = ∅ :=
  rfl

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

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

Разделы

Аффилиация

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