restrict_mrange — Mathlib

English

For f : M →* N, the range of the restricted map equals the image of the restricting submonoid: mrange (f.restrict S) = S.map f.

Русский

Для f : M →* N образ ограниченного отображения равен образу S подмножества: mrange (f.restrict S) = S.map f.

LaTeX

$$$$ \\mathrm{mrange}(f\\restriction S) = S.\\mathrm{map}\;f $$$$

Lean4

@[to_additive (attr := simp)]
theorem restrict_mrange (f : M →* N) : mrange (f.restrict S) = S.map f := by simp [SetLike.ext_iff]

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