ext

Mathlib.Topology.ContinuousMap.Defs

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

English

Two continuous maps f,g are equal if they agree at every point: if f(a) = g(a) for all a ∈ X, then f = g.

Русский

Две непрерывные карты равны, если они совпадают в каждой точке: если f(a) = g(a) для всех a ∈ X, тогда f = g.

LaTeX

$$$\\forall a, f(a)=g(a) \\implies f=g$$$

Lean4

@[ext]
theorem ext {f g : C(X, Y)} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext _ _ h

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

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

Разделы

Аффилиация

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