elim3

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#Or.elim3

English

If h: a ∨ b ∨ c, and ha: a → d, hb: b → d, hc: c → d, then d.

Русский

Если h: a ∨ b ∨ c, ha: a → d, hb: b → d, hc: c → d, тогда d.

LaTeX

$${c d : Prop} (h : a \\lor (b \\lor c)) (ha : a \\to d) (hb : b \\to d) (hc : c \\to d) : d$$

Lean4

theorem elim3 {c d : Prop} (h : a ∨ b ∨ c) (ha : a → d) (hb : b → d) (hc : c → d) : d :=
  Or.elim h ha fun h₂ ↦ Or.elim h₂ hb hc

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

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

Разделы

Аффилиация

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