coe_coe

Mathlib.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#OrderHomClass.coe_coe

English

For any suitable f, the coerced function equals f.

Русский

Для любого подходящего f равенство коe(f) = f.

LaTeX

$$$\\forall f:\\ F, \\ ⇑(f: α \\to_o β) = f$.$$

Lean4

@[simp]
theorem _root_.OrderHomClass.coe_coe {F} [FunLike F α β] [OrderHomClass F α β] (f : F) : ⇑(f : α →o β) = f :=
  rfl

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

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

Разделы

Аффилиация

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