range_add_le — Mathlib

English

For f,g with same domain, range(f + g) ≤ range f ⊔ range g; the range of the sum is contained in the join of the ranges.

Русский

Для отображений f,g: range(f+g) ⊆ range f ⊔ range g; образ суммы содержится в их объединении.

LaTeX

$$$\operatorname{range}(f + g) \leq \operatorname{range}(f) \sqcup \operatorname{range}(g)$$$

Lean4

theorem range_add_le [RingHomSurjective τ₁₂] (f g : M →ₛₗ[τ₁₂] M₂) : range (f + g) ≤ range f ⊔ range g :=
  by
  rintro - ⟨_, rfl⟩
  apply add_mem_sup
  all_goals simp only [mem_range, exists_apply_eq_apply]

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