ite_eq_iff'

Mathlib.Logic.Basic

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

English

The equality (ite P a b) = c holds iff (P → a=c) and (¬P → b=c).

Русский

Равенство (ite P a b) = c верно тогда, когда P → a=c и ¬P → b=c.

LaTeX

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

Lean4

theorem ite_eq_iff' : ite P a b = c ↔ (P → a = c) ∧ (¬P → b = c) :=
  dite_eq_iff'

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

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

Разделы

Аффилиация

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