eq_bot_iff — Mathlib

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

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