coe_transContinuousLinearEquiv_symm

English

The inverse of the transported model satisfies (I.transContinuousLinearEquiv e).symm = I.symm ∘ e.symm; i.e., the coordinate change induced by the inverse linear isomorphism composes with the inverse of the original model.

Русский

Обратное преобразование модели удовлетворяет (I.transContinuousLinearEquiv e).symm = I.symm ∘ e.symm; координатное изменение, заданное обратным линейным изоморфизмом, композиционно соответствует обратному исходной модели.

LaTeX

$$$\bigl(I.transContinuousLinearEquiv e\bigr)^{-1} = I^{-1} \circ e^{-1}$$$

Lean4

@[simp, mfld_simps]
theorem coe_transContinuousLinearEquiv_symm : ⇑(I.transContinuousLinearEquiv e).symm = I.symm ∘ e.symm :=
  rfl

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