ite_eq_iff

Mathlib.Logic.Basic

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

English

The value of the ordinary if-then-else equals c iff either P and a=c or not P and b=c.

Русский

Значение оператора if равняется c тогда, когда либо P и a=c, либо не-P и b=c.

LaTeX

$$$(\mathrm{ite}\, P\, a\, b)=c \iff (P\land a=c) \lor (\lnot P\land b=c).$$$

Lean4

theorem ite_eq_iff : ite P a b = c ↔ P ∧ a = c ∨ ¬P ∧ b = c :=
  dite_eq_iff.trans <| by rw [exists_prop, exists_prop]

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

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

Разделы

Аффилиация

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