ker_prod_ker_le_ker_coprod — Mathlib

English

If f: M →L[R] M2 and g: M →L[R] M3 are linear maps and ker f ⊔ ker g = ⊤, then the range of the combined map f.prod g equals the product of their ranges.

Русский

Пусть f: M →L[R] M2 и g: M →L[R] M3. Если сумма ядер ker f ⊔ ker g = ⊤, то образ объединённого отображения f.prod g равен произведению образов: range(f.prod g) = range(f) × range(g).

LaTeX

$$$$ \mathrm{range}(f \prod g) = \mathrm{range}(f) \;\mathrm{prod}\; \mathrm{range}(g) $$$$

Lean4

theorem ker_prod_ker_le_ker_coprod (f : M →L[R] M₃) (g : M₂ →L[R] M₃) :
    (LinearMap.ker f).prod (LinearMap.ker g) ≤ LinearMap.ker (f.coprod g) :=
  LinearMap.ker_prod_ker_le_ker_coprod f.toLinearMap g.toLinearMap

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