coe_srange — Mathlib

English

For a semigroup hom f: M → N, the underlying set of its image equals the set of all values f(m) as m varies in M; i.e., the range of f as a function equals its srange.

Русский

Для полугомомера μ: M → N множество значений образа совпадает с диапазоном функции μ; то есть srange μ является диапазоном функции.

LaTeX

$$$(f.srange : \mathrm{Set}\ N) = \mathrm{Set.range}\, f$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_srange (f : M →ₙ* N) : (f.srange : Set N) = Set.range f :=
  rfl

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