elim

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#BEx.elim

English

If there exists x with p x and h : p x, and if for all a with p a we have P a h → b, then b.

Русский

Если существует x с p x и h : p x, и если для каждого a с p a верно P a h → b, тогда следует b.

LaTeX

$$$(\exists x\, h, P x h) \to (\forall a\, h, P a h \to b) \to b$$

Lean4

theorem elim {b : Prop} : (∃ x h, P x h) → (∀ a h, P a h → b) → b
  | ⟨a, h₁, h₂⟩, h' => h' a h₁ h₂

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

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

Разделы

Аффилиация

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