range_image — Mathlib

English

The range of the image operator equals the power set of the range of f: range (image f) = P(range f).

Русский

Диапазон оператора образа равен множеству подмножеств диапазона функции: range(image f) = P(range f).

LaTeX

$$$ \\mathrm{range}(\\mathrm{image}(f)) = \\mathcal{P}(\\mathrm{range}(f)). $$$

Lean4

theorem range_image (f : α → β) : range (image f) = 𝒫 range f :=
  ext fun _ => subset_range_iff_exists_image_eq.symm

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