coe_himp

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#Sublocale.coe_himp

English

The underlying value of the internal implication equals the ambient implication: (a ⇨ b).val = a.val ⇨ b.val.

Русский

Значение внутренней импликации равно импликации в X: (a ⇨ b).val = a.val ⇨ b.val.

LaTeX

$$$(a \Rightarrow b).\text{val} = a.\text{val} \Rightarrow b.\text{val}$$$

Lean4

@[simp, norm_cast]
theorem coe_himp (a b : S) : (a ⇨ b).val = a.val ⇨ b.val :=
  rfl

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

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

Разделы

Аффилиация

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