decide_congr — Mathlib

English

If p and q are decidable propositions and p ↔ q, then decide(p) = decide(q).

Русский

Если p и q — разрешимые пропозиции и p ⇔ q, тогда decide(p) = decide(q).

LaTeX

$$$$ \forall p\, q\, [\operatorname{Decidable}(p)]\,[\operatorname{Decidable}(q)]\,(p \leftrightarrow q)\Rightarrow \operatorname{decide}(p) = \operatorname{decide}(q) $$$$

Lean4

theorem decide_congr {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : decide p = decide q :=
  decide_eq_decide.mpr h

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