contDiff_prodAssoc — Mathlib

English

The reverse equivalence (E × (F × G)) ≃ ((E × F) × G) is smooth.

Русский

Обратное эквивалентное преобразование гладко.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}} n ((\mathrm{prodAssoc}\; E\; F\; G)^{\,-1})$$$

Lean4

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

Warning: if you think you need this lemma, it is likely that you can simplify your proof by
reformulating the lemma that you're applying next using the tips in
Note [continuity lemma statement]
-/
theorem contDiff_prodAssoc {n : WithTop ℕ∞} : ContDiff 𝕜 n <| Equiv.prodAssoc E F G :=
  (LinearIsometryEquiv.prodAssoc 𝕜 E F G).contDiff

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