map_add_le — Mathlib

English

For any f,g and any submodule p, the image of p under the sum map is contained in the sum of the images: map (f+g) p ⊆ map f p ⊔ map g p.

Русский

Образ p под отображением суммы лежит внутри сумма образов: map (f+g) p ⊆ map f p ⊔ map g p.

LaTeX

$$$\\operatorname{map}(f+g,p) \\leq \\operatorname{map} f(p) \\cup \\operatorname{map} g(p)$$

Lean4

theorem map_add_le (f g : M →ₛₗ[σ₁₂] M₂) : map (f + g) p ≤ map f p ⊔ map g p :=
  by
  rintro x ⟨m, hm, rfl⟩
  exact add_mem_sup (mem_map_of_mem hm) (mem_map_of_mem hm)

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