ext

Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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

English

For any X, its toFun component equals the function obtained by coercion, i.e., X.toFun = ⇑X.

Русский

Для любого X его компонент toFun равен функции, полученной преобразованием: X.toFun = ⇑X.

LaTeX

$$$X^{\mathrm{toFun}} = X$ as functions$$

Lean4

@[ext]
theorem ext (h : ∀ f, X f = Y f) : X = Y :=
  DFunLike.ext _ _ h

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

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

Разделы

Аффилиация

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