map_isFunc — Mathlib

English

IsFunc x y (map f x) iff ∀ z ∈ x, f z ∈ y.

Русский

IsFunc x y (map f x) эквивалентно ∀ z ∈ x, f z ∈ y.

LaTeX

$$$\\text{IsFunc }\\ x\\ y\\ (\\mathrm{map}\\ f\\ x) \\iff \\forall z \\in x, f z \\in y$$$

Lean4

@[simp]
theorem map_isFunc {f : ZFSet → ZFSet} [Definable₁ f] {x y : ZFSet} : IsFunc x y (map f x) ↔ ∀ z ∈ x, f z ∈ y :=
  ⟨fun ⟨ss, h⟩ z zx =>
    let ⟨_, t1, t2⟩ := h z zx
    (t2 (f z) (image.mk _ _ zx)).symm ▸ (pair_mem_prod.1 (ss t1)).right,
    fun h =>
    ⟨fun _ yx =>
      let ⟨z, zx, ze⟩ := mem_image.1 yx
      ze ▸ pair_mem_prod.2 ⟨zx, h z zx⟩,
      fun _ => map_unique⟩⟩

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