ext

Mathlib.Geometry.Manifold.ContMDiffMap

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

English

Two ContMDiffMaps are equal if they are equal at every point.

Русский

Два отображения ContMDiffMap равны, если совпадают на каждой точке.

LaTeX

$$$(\forall x: M, f x = g x) \Rightarrow f = g$$$

Lean4

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

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

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

Разделы

Аффилиация

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