exists

Mathlib.Logic.ExistsUnique

URI: https://scilib.ai/kg/mathlib#ExistsUnique.exists

English

From ∃! x, p x we obtain ∃ x, p x.

Русский

Из существования единственного x с p(x) следует существование некоторого x с p(x).

LaTeX

$$$$(\\\\exists! x, p(x)) \Rightarrow (\\\\exists x, p(x)).$$$$

Lean4

theorem «exists» {p : α → Prop} : (∃! x, p x) → ∃ x, p x
  | ⟨x, h, _⟩ => ⟨x, h⟩

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

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

Разделы

Аффилиация

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