imp_congr_eq

Mathlib.Logic.Basic

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

English

If a=c and b=d, then (a → b) = (c → d).

Русский

Если a = c и b = d, то (a → b) = (c → d).

LaTeX

$$$(a \to b) = (c \to d)$$$

Lean4

theorem imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) :=
  propext (imp_congr h₁.to_iff h₂.to_iff)

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

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

Разделы

Аффилиация

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