ite_prop_iff_and

Mathlib.Logic.Basic

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

English

The statement (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 \big((P \to Q) \land (\lnot P \to R)\big)$$$

Lean4

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

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

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

Разделы

Аффилиация

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