English
The empty dependent product over a dependent family β: α → Sort* is the unique function defined on the empty index set; in particular, there is exactly one function f: ∅ → β(a) for each a, so the empty product yields a singleton.
Русский
Пусть β: α → Sort*. Пустое зависимое произведение над пустым индексным множеством эквивалентно единственному функциям на пустом множестве; то есть существует ровно одна функция f: ∅ → β(a).
LaTeX
$$$\\text{There is a unique } f: \\emptyset \\to \\beta. $$$
Lean4
/-- The empty dependent product function, defined on the empty set. The assumption `a ∈ ∅` is never
satisfied. -/
def empty (β : α → Sort*) (a : α) (h : a ∈ (∅ : Finset α)) : β a :=
Multiset.Pi.empty β a h
