ext' — Mathlib

English

If two function-like objects have identical underlying functions, then they are equal.

Русский

Если два объекта типа F имеют одинаковые значения на каждом аргументе, то они равны.

LaTeX

$$$\forall f,g \in F, \ (f : \prod_{a:\alpha} \beta(a)) = (g : \prod_{a:\alpha} \beta(a)) \Rightarrow f = g.$$$

Lean4

theorem ext' {f g : F} (h : (f : ∀ a : α, β a) = (g : ∀ a : α, β a)) : f = g :=
  DFunLike.coe_injective' h

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