by_cases

Mathlib.Logic.Basic

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

English

If p implies q and not p implies q, then q.

Русский

Если p ⇒ q и ¬p ⇒ q, то q.

LaTeX

$$$(p \to q) \to (\neg p \to q) \to q$$$

Lean4

theorem by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
  open scoped Classical in if hp : p then hpq hp else hnpq hp

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

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

Разделы

Аффилиация

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