ext

Mathlib.Data.FunLike.Basic

URI: https://scilib.ai/kg/mathlib#DFunLike.ext

English

If two function-like objects agree on every input, they are equal.

Русский

Если два объекта F совпадают на каждом входе, то они равны.

LaTeX

$$$\forall f,g \in F, \ (\forall x:\alpha, f(x) = g(x)) \Rightarrow f = g.$$$

Lean4

theorem ext (f g : F) (h : ∀ x : α, f x = g x) : f = g :=
  DFunLike.coe_injective' (funext h)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru