pimage_empty

Mathlib.Data.Finset.PImage

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

English

The pimage of the empty Finset is empty: pimage f ∅ = ∅.

Русский

Pimage от пустого Finset равно пустому множеству: pimage f ∅ = ∅.

LaTeX

$$$pimage\ f\ \emptyset = \emptyset$.$$

Lean4

@[simp]
theorem pimage_empty : pimage f ∅ = ∅ := by
  ext
  simp

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

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

Разделы

Аффилиация

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