ite_and

Mathlib.Logic.Basic

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

English

The expression ite (P ∧ Q) a b equals ite P (ite Q a b) b, assuming decidability of P and Q.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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