range_coprod — Mathlib

English

The range of a coprod equals the join of the ranges: range(f1 coprod f2) = range f1 ⊔ range f2.

Русский

Образ копрода равен объединению образов: range(f1 coprod f2) = range f1 ⊔ range f2.

LaTeX

$$$$ \mathrm{range}(f_1.coprod f_2) = \mathrm{range}(f_1) \;\sqcup\; \mathrm{range}(f_2) $$$$

Lean4

theorem range_coprod (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) : range (f₁.coprod f₂) = range f₁ ⊔ range f₂ :=
  LinearMap.range_coprod ..

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