graphOn_empty

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.graphOn_empty

English

The graph of f on the empty set is empty: graphOn f ∅ = ∅.

Русский

График функции f на пустом множестве пуст.

LaTeX

$$$$ \\mathrm{graphOn} f \\emptyset = \\emptyset. $$$$

Lean4

@[simp]
theorem graphOn_empty (f : α → β) : graphOn f ∅ = ∅ :=
  image_empty _

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

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

Разделы

Аффилиация

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