exists — Mathlib

English

If f is surjective, then exists y with p(y) iff exists x with p(f(x)).

Русский

Если f сюръективна, то существует y с p(y) тогда и только тогда, когда существует x с p(f(x)).

LaTeX

$$$\\operatorname{Surjective}(f) \\rightarrow (\\exists y\, p(y) \\iff \\exists x\, p(f(x)))$$$

Lean4

protected theorem «exists» (hf : Surjective f) {p : β → Prop} : (∃ y, p y) ↔ ∃ x, p (f x) :=
  ⟨fun ⟨y, hy⟩ ↦
    let ⟨x, hx⟩ := hf y
    ⟨x, hx.symm ▸ hy⟩,
    fun ⟨x, hx⟩ ↦ ⟨f x, hx⟩⟩

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