mkD_eq_self

Mathlib.Topology.ContinuousMap.Basic

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

English

If f is continuous, then the glueing operator mkD applied to f and any g yields f; i.e., mkD(f,g) = f.

Русский

Если f непрерывна, то оператор склейки mkD, применяемый к f и произвольному g, даёт f; то есть mkD(f,g) = f.

LaTeX

$$$\\mathrm{mkD}(f,g) = f$$$

Lean4

theorem mkD_eq_self {f g : C(α, β)} : mkD f g = f :=
  mkD_of_continuous f.continuous

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

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

Разделы

Аффилиация

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