ext — Mathlib

English

Two dependent finite-support functions are equal if they agree at every index: if f i = g i for all i, then f = g.

Русский

Две зависимые функции с конечной опорой равны, если их значения совпадают на каждом индексе: если f i = g i для всех i, то f = g.

LaTeX

$$$ \forall i, f i = g i \implies f = g $$$

Lean4

@[ext]
theorem ext {f g : Π₀ i, β i} (h : ∀ i, f i = g i) : f = g :=
  DFunLike.ext _ _ h

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