English
In a Pi-type product, f equals the bottom element iff every coordinate f(i) equals the bottom element.
Русский
В произведении типа Pi функция f равна нулю тогда и только тогда, когда каждый компонент f(i) равен нижнему элементу.
LaTeX
$$$ \forall i, f(i) = \\bot \\quad \\Longleftrightarrow \\quad f = \\bot $$$
Lean4
protected theorem eq_bot_iff [∀ i, Bot (π i)] {f : ∀ i, π i} : f = ⊥ ↔ ∀ i, f i = ⊥ :=
funext_iff