mem_image — Mathlib

English

For a function f, y ∈ image f x is equivalent to there exists z ∈ x with y ≃ f(z).

Русский

Для функции f: y принадлежит image f x тогда и только тогда, когда существует z ∈ x такое, что y ≃ f(z).

LaTeX

$$$$ y \in \mathrm{image}(f)(x) \iff \exists z \in x,\; y \equiv f(z) $$$$

Lean4

theorem mem_image {f : PSet.{u} → PSet.{u}} (H : ∀ x y, Equiv x y → Equiv (f x) (f y)) :
    ∀ {x y : PSet.{u}}, y ∈ image f x ↔ ∃ z ∈ x, Equiv y (f z)
  | ⟨_, A⟩, _ => ⟨fun ⟨a, ya⟩ => ⟨A a, Mem.mk A a, ya⟩, fun ⟨_, ⟨a, za⟩, yz⟩ => ⟨a, yz.trans <| H _ _ za⟩⟩

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