range_prod_le — Mathlib

English

For linear maps f: M → M₂ and g: M → M₃, the range of the pair map satisfies range(prod f g) ⊆ range f × range g.

Русский

Для линейных отображений f: M → M₂ и g: M → M₃ верно, что образ пары отображений ограничивает произведение образов: range(prod f g) ⊆ range f × range g.

LaTeX

$$$\\mathrm{range}(\\mathrm{prod}(f,g)) \\subseteq \\mathrm{range}(f) \\times \\mathrm{range}(g).$$$

Lean4

theorem range_prod_le (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : range (prod f g) ≤ (range f).prod (range g) :=
  by
  simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp]
  rintro _ x rfl
  exact ⟨⟨x, rfl⟩, ⟨x, rfl⟩⟩

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