some_spec₂

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#Classical.some_spec₂

English

In classical logic, given h : Exists (λ a, p a) and hpq : ∀ a, p a → q a, then q (choose h).

Русский

В классической логике, при h : Exists (λ a, p a) и hpq : ∀ a, p a → q a, тогда выполняется q(choose h).

LaTeX

$$q(\mathrm{choose}(h))$$

Lean4

theorem some_spec₂ {α : Sort*} {p : α → Prop} {h : ∃ a, p a} (q : α → Prop) (hpq : ∀ a, p a → q a) : q (choose h) :=
  hpq _ <| choose_spec _

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

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

Разделы

Аффилиация

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