range_id

Mathlib.Algebra.Module.Submodule.Range

URI: https://scilib.ai/kg/mathlib#LinearMap.range_id

English

For linear maps f: M → M2 and g: M2 → M3, range(g ∘ f) = map g (range f).

Русский

Для линейных отображений f: M → M2 и g: M2 → M3 выполнено range(g ∘ f) = map g (range f).

LaTeX

$$$\operatorname{range}(g \circ f) = \operatorname{map} g (\operatorname{range} f)$$$

Lean4

@[simp]
theorem range_id : range (LinearMap.id : M →ₗ[R] M) = ⊤ :=
  SetLike.coe_injective Set.range_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru