exists_mem_image — Mathlib

English

There exists a y in image f s such that p(y) holds iff there exists x in s with p(f(x)).

Русский

Существует y в image f s с p(y) выполняющимся тогда и только тогда, когда существует x в s с p(f(x)).

LaTeX

$$$\\exists y \\in \\operatorname{image}(f,s), p(y) \\iff \\exists x \\in s, p(f(x))$$$

Lean4

theorem exists_mem_image {p : β → Prop} : (∃ y ∈ s.image f, p y) ↔ ∃ x ∈ s, p (f x) := by simp

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