ne_iff — Mathlib

English

In the DFinsupp space, two dependent functions are not equal iff there exists an index i where they differ.

Русский

В пространстве DFinsupp два зависимых отображения не равны тогда, когда существует хотя бы один индекс, на котором они различаются.

LaTeX

$$$ f \neq g \iff \exists i, f i \neq g i $$$

Lean4

theorem ne_iff {f g : Π₀ i, β i} : f ≠ g ↔ ∃ i, f i ≠ g i :=
  DFunLike.ne_iff

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