swap

Mathlib.Geometry.Manifold.ContMDiff.Constructions

URI: https://scilib.ai/kg/mathlib#ContMDiff.swap

English

The swap map on a double sum is ContMDiff: ContMDiff.swap = ContMDiff.sumElim inl inr.

Русский

Обменная карта на двойной сумме гладкая: swap = sumElim inl inr.

LaTeX

$$$ ContMDiff.swap : ContMDiff I I n (Sum.swap M M') $$$

Lean4

theorem swap : ContMDiff I I n (@Sum.swap M M') :=
  ContMDiff.sumElim inr inl

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

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

Разделы

Аффилиация

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