toSet_image — Mathlib

English

For any definable function f from ZFSet to ZFSet and any x, the underlying set of the image of x under f equals the image of x's underlying set: (toSet(image f x)) = Set.image f (x.toSet).

Русский

Для любой определимой функции f: ZFSet → ZFSet и любого x справедливо: toSet(image f x) = Set.image f (x.toSet).

LaTeX

$$$ (\\\\mathrm{toSet}(\\\\mathrm{image} f x)) = \\\\mathrm{Set.image} f (x.toSet). $$$

Lean4

@[simp]
theorem toSet_image (f : ZFSet → ZFSet) [Definable₁ f] (x : ZFSet) : (image f x).toSet = f '' x.toSet :=
  by
  ext
  simp

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