ext'_iff

Mathlib.Data.FunLike.Basic

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

English

Two function-like objects are equal iff their underlying functions are equal.

Русский

Два объекта типа F равны тогда и только тогда, когда их базовые функции равны.

LaTeX

$$$f = g \iff (f : \prod_{a:\alpha} \beta(a)) = (g : \prod_{a:\alpha} \beta(a)).$$$

Lean4

theorem ext'_iff {f g : F} : f = g ↔ (f : ∀ a : α, β a) = (g : ∀ a : α, β a) :=
  coe_fn_eq.symm

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

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

Разделы

Аффилиация

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