if_congr

Mathlib.Logic.Basic

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

English

If P and Q are equivalent and x = u, y = v, then ite P x y = ite Q u v.

Русский

Если P и Q эквивалентны и x = u, y = v, то ite P x y = ite Q u v.

LaTeX

$$$\text{If } P \iff Q, \ x = u, \ y = v \Rightarrow \operatorname{ite} P x y = \operatorname{ite} Q u v$$$

Lean4

theorem if_congr (h_c : P ↔ Q) (h_t : x = u) (h_e : y = v) : ite P x y = ite Q u v :=
  if_ctx_congr h_c (fun _ ↦ h_t) (fun _ ↦ h_e)

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

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

Разделы

Аффилиация

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