mem_image — Mathlib

English

y ∈ image f x iff ∃ z ∈ x, f z = y.

Русский

y принадлежит образу f на x тогда и только тогда, когда существует z ∈ x такое, что f z = y.

LaTeX

$$$y \\in \\mathrm{image}\\ f\\ x \\iff \\exists z \\in x, f z = y$$$

Lean4

@[simp]
theorem mem_image {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x y : ZFSet.{u}} : y ∈ image f x ↔ ∃ z ∈ x, f z = y :=
  Quotient.inductionOn₂ x y fun ⟨_, A⟩ _ =>
    ⟨fun ⟨a, ya⟩ => ⟨⟦A a⟧, Mem.mk A a, ((Quotient.sound ya).trans Definable₁.mk_out).symm⟩, fun ⟨_, hz, e⟩ =>
      e ▸ image.mk _ _ hz⟩

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