exists_mem_of_exists — Mathlib

English

If p x holds for all x, then from the existence of some x with q x it follows that there exists x with p x and q x.

Русский

Если p(x) истинно для всех x, то существование некоторого x с q(x) влечет существование x с p(x) и q(x).

LaTeX

$$$\bigl(\forall x\, p(x)\bigr)\to\bigl((\exists x\, q(x))\to (\exists x\, p(x)\land q(x))\bigr)$$$

Lean4

theorem exists_mem_of_exists (H : ∀ x, p x) : (∃ x, q x) → ∃ (x : _) (_ : p x), q x
  | ⟨x, hq⟩ => ⟨x, H x, hq⟩

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