ite_prop_iff_or

Mathlib.Logic.Basic

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

English

The proposition (if P then Q else R) is equivalent to (P ∧ Q) ∨ (¬P ∧ R).

Русский

Предикат (если P тогда Q иначе R) эквивалентен (P ∧ Q) ∨ (¬P ∧ R).

LaTeX

$$$\big(\text{if } P \text{ then } Q \text{ else } R\big) \iff (P \land Q) \lor (\lnot P \land R)$$$

Lean4

theorem ite_prop_iff_or : (if P then Q else R) ↔ (P ∧ Q ∨ ¬P ∧ R) := by by_cases p : P <;> simp [p]

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

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

Разделы

Аффилиация

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