exists_of_exists_mem

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#exists_of_exists_mem

English

If there exists x with p x and q x, then there exists x with q x.

Русский

Если существует x, на котором выполняются p x и q x, то существует x, на котором выполняется q x.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru