exists_range_iff — Mathlib

English

There exists y in the range with property p(y) if and only if there exists x with p(f(x)).

Русский

Существует y в диапазоне с свойством p(y) тогда и только тогда, когда существует x с p(f(x)).

LaTeX

$$$\\exists y \\in f.range \\; p(y) \\;\\Leftrightarrow\\; \\exists x, p(f(x))$$$

Lean4

theorem exists_range_iff {f : α →ₛ β} {p : β → Prop} : (∃ y ∈ f.range, p y) ↔ ∃ x, p (f x) := by
  simpa only [mem_range, exists_prop] using Set.exists_range_iff

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