ext — Mathlib

English

Extensionality for arrows: if two arrows have equal components at every index i, then they are equal.

Русский

Расширение стрелок: если две стрелки имеют одинаковые компоненты на каждом индексе i, то они равны.

LaTeX

$$For all f,g : α.Arrow β, if ∀ i : Fin2 n, f i = g i, then f = g.$$

Lean4

/-- Extensionality for arrows -/
@[ext]
theorem ext {α β : TypeVec n} (f g : α ⟹ β) : (∀ i, f i = g i) → f = g := by intro h; funext i; apply h

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