contDiff_prodAssoc_symm — Mathlib

English

The symmetry map (E × (F × G)) ≃ ((E × F) × G) is smooth.

Русский

Симметрия пространства сопряжена с гладкостью.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}} n ((\mathrm{prodAssoc}\; E\; F\; G).symm)$$$

Lean4

/-- The natural equivalence `E × (F × G) ≃ (E × F) × G` is smooth.

Warning: see remarks attached to `contDiff_prodAssoc`
-/
theorem contDiff_prodAssoc_symm {n : WithTop ℕ∞} : ContDiff 𝕜 n <| (Equiv.prodAssoc E F G).symm :=
  (LinearIsometryEquiv.prodAssoc 𝕜 E F G).symm.contDiff

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