range_coe — Mathlib

English

For any L-hom f from M to N, the underlying set of the range equals the standard image of f, i.e., range f as a Set equals the image Set.range f.

Русский

Для любого гомоморфизма f: M → N множество образа совпадает с обычным образом функции; то есть range f как множество равно Set.range f.

LaTeX

$$$ \operatorname{range}(f) = \{ f(x) : x \in M \} $$$

Lean4

theorem range_coe (f : M →[L] N) : (range f : Set N) = Set.range f :=
  rfl

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