transContinuousLinearEquiv_range — Mathlib

English

For a model I and linear isomorphism e, the range of the transported model equals the image of the original range under e: range(I.transContinuousLinearEquiv e) = e''range(I).

Русский

Для модели I и линейного изоморфизма e образ диапазона преобразованной модели равен изображению исходного диапазона под действием e: range(I.transContinuousLinearEquiv e) = e''range(I).

LaTeX

$$$\mathrm{range}\bigl(I.transContinuousLinearEquiv e\bigr) = e''\mathrm{range}(I)$$$

Lean4

theorem transContinuousLinearEquiv_range : range (I.transContinuousLinearEquiv e) = e '' range I :=
  range_comp e I

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