if_ctx_congr — Mathlib

English

If two propositions P and Q are equivalent, then equivalent contexts imply equal results for corresponding conditional expressions.

Русский

Если P и Q эквивалентны, то при эквивалентности условий контекста равны результаты для соответствующих условных выражений.

LaTeX

$$$\text{If } P \leftrightarrow Q, \ (Q \Rightarrow (x = u)) \Rightarrow ((\lnot Q) \Rightarrow (y = v)) \Rightarrow \operatorname{ite} P x y = \operatorname{ite} Q u v$$$

Lean4

theorem if_ctx_congr (h_c : P ↔ Q) (h_t : Q → x = u) (h_e : ¬Q → y = v) : ite P x y = ite Q u v :=
  ite_congr h_c.eq h_t h_e

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