exists₂ — Mathlib

English

If there exists a unique x with ∃! hx : p x, q x hx, then there exist x and hx such that p x and q x hx.

Русский

Если есть уникальное сочетание x и hx: p(x), q(x,hx), то существует x и hx такие, что p(x) и q(x,hx).

LaTeX

$$$$ \\exists! x, \\exists! hx : p(x), q(x,hx) \\Rightarrow \\exists x, \\exists hx: p(x), q(x,hx). $$$$

Lean4

theorem exists₂ {p : α → Sort*} {q : ∀ (x : α) (_ : p x), Prop} (h : ∃! x, ∃! hx : p x, q x hx) :
    ∃ (x : _) (hx : p x), q x hx :=
  h.exists.imp fun _ hx ↦ hx.exists

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