symm_trans' — Mathlib

English

The range of the composed map equals the preimage of the range under the inverse diffeomorphism.

Русский

Диапазон композиции равен предобразу диапазона под обратным диффеоморфизмом.

LaTeX

$$$\operatorname{range}(h_1 \circ f) = h_1^{-1}(\operatorname{range} f).$$$

Lean4

@[simp]
theorem symm_trans' (h₁ : M ≃ₘ^n⟮I, I'⟯ M') (h₂ : M' ≃ₘ^n⟮I', J⟯ N) : (h₁.trans h₂).symm = h₂.symm.trans h₁.symm :=
  rfl

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