contMDiff_comp_diffeomorph_iff — Mathlib

English

The underlying equivalence of the homeomorphism produced by a diffeomorphism equals the original equivalence.

Русский

Унитарная эквивалентность гомеоморфизма, полученного из диффеоморфизма, равна исходной эквивалентности.

LaTeX

$$h.toHomeomorph.toEquiv = h.toEquiv$$

Lean4

@[simp]
theorem contMDiff_comp_diffeomorph_iff {m} (h : M ≃ₘ^n⟮I, J⟯ N) {f : N → M'} (hm : m ≤ n) :
    ContMDiff I I' m (f ∘ h) ↔ ContMDiff J I' m f :=
  h.toEquiv.forall_congr fun _ ↦ h.contMDiffAt_comp_diffeomorph_iff hm

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