ite_or

Mathlib.Logic.Basic

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

English

The expression ite (P ∨ Q) a b equals ite P a (ite Q a b), given decidability of P and Q.

Русский

Выражение ite (P ∨ Q) a b равно ite P a (ite Q a b) при разрешимости P и Q.

LaTeX

$$$\ite (P \lor Q) a b = \ite P a (\ite Q a b)$$$

Lean4

theorem ite_or : ite (P ∨ Q) a b = ite P a (ite Q a b) := by by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]

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

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

Разделы

Аффилиация

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