copy_eq

Mathlib.Order.Hom.BoundedLattice

URI: https://scilib.ai/kg/mathlib#SupBotHom.copy_eq

English

Let f be a SupBotHom α β and f' a function α → β with h: f' = f. Then f.copy f' h = f.

Русский

Пусть f — SupBotHom(α,β) и f' : α → β; если h: f' = f, то f.copy f' h = f.

LaTeX

$$$\\forall f:\\mathrm{SupBotHom}(\\alpha,\\beta),\\forall f':\\alpha\\to\\beta,\\forall h:\\,f'=f,\\ f.copy f' h = f$$$

Lean4

theorem copy_eq (f : SupBotHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

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

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

Разделы

Аффилиация

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