map_srange — Mathlib

English

The same statement as above: the image under a composed map equals the range of the composition.

Русский

Та же самая идея: образ под действием композиции равен диапазону композиции.

LaTeX

$$map_srange (g) (f) : map g (srange f) = srange (g.comp f)$$

Lean4

theorem map_srange (g : S →ₙ+* T) (f : R →ₙ+* S) : map g (srange f) = srange (g.comp f) := by
  simpa only [srange_eq_map] using (⊤ : NonUnitalSubsemiring R).map_map g f

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