map_rangeS — Mathlib

English

For f: R → S and g: S → T, the image rangeS(f) mapped by g equals the rangeS of the composition, i.e., rangeS(f).map g = rangeS(g ∘ f).

Русский

Для отображений f: R → S и g: S → T образ rangeS(f), подвергшийся отображению g, равен rangeS(g ∘ f).

LaTeX

$$$ \operatorname{rangeS}(f).\operatorname{map} g = \operatorname{rangeS}(g \circ f) $$$

Lean4

theorem map_rangeS : f.rangeS.map g = (g.comp f).rangeS := by
  simpa only [rangeS_eq_map] using (⊤ : Subsemiring R).map_map g f

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