coe_transContinuousLinearEquiv — Mathlib

English

Let e be a continuous linear isomorphism between vector spaces and I a model with corners. The transported model I.transContinuousLinearEquiv e has as its underlying map the composition e ∘ I, i.e., applying the original model map and then the linear isomorphism.

Русский

Пусть e — непрерывная линейная изоморфизм между пространствами, а I — модель с углами. Преобразованная модель I.transContinuousLinearEquiv e имеет как базовую отображение композицию e ∘ I, то есть применение исходной карты модели, затем линейного изоморфизма.

LaTeX

$$$\forall x,\ (I\;\text{transContinuousLinearEquiv}\;e)(x) = e\bigl(I(x)\bigr)$$$

Lean4

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

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