symm_apply_apply — Mathlib

English

The underlying function of a composed pair of diffeomorphisms is the composition of the underlying functions.

Русский

Основанная функция композиции двух диффеоморфизмов есть композиция их функций.

LaTeX

$$$((h_1.trans h_2)^\text{underlying}) = h_2^{\text{underlying}} \circ h_1^{\text{underlying}}.$$$

Lean4

@[simp]
theorem symm_apply_apply (h : M ≃ₘ^n⟮I, J⟯ N) (x : M) : h.symm (h x) = x :=
  h.toEquiv.symm_apply_apply x

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