English
For a definable function f and y ∈ x, the fval of the mapped y equals f(y): (Class.ofSet (ZFSet.map f x)).fval (Class.ofSet y) = Class.ofSet (f y).
Русский
Пусть f определима, и y ∈ x; значение f на y совпадает с преобразованием через f: (Class.ofSet (ZFSet.map f x)).fval (Class.ofSet y) = Class.ofSet (f y).
LaTeX
$$$ \\bigl( (\\mathrm{Class.ofSet}(\\mathrm{ZFSet.map} f x)) . \\mathrm{fval} (\\mathrm{Class.ofSet} y) \\bigr) = \\mathrm{Class.ofSet}(f y). $$$
Lean4
@[simp]
theorem map_fval {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x y : ZFSet.{u}} (h : y ∈ x) :
(ZFSet.map f x ′ y : Class.{u}) = f y :=
Class.iota_val _ _ fun z => by
rw [Class.toSet_of_ZFSet, Class.coe_apply, mem_map]
exact
⟨fun ⟨w, _, pr⟩ => by
let ⟨wy, fw⟩ := ZFSet.pair_injective pr
rw [← fw, wy], fun e => by
subst e
exact ⟨_, h, rfl⟩⟩
