copy_eq

Mathlib.Order.Hom.BoundedLattice

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

English

Let f,g: InfTopHom α β. If f(a) = g(a) for all a, then f = g.

Русский

Пусть f,g: InfTopHom(α,β). Тогда если f(a) = g(a) для всех a, то f = g.

LaTeX

$$$\\forall f,g:\\mathrm{InfTopHom}(\\alpha,\\beta),\\ (\\forall a:\\alpha,\\ f(a)=g(a)) \\Rightarrow f=g$$$

Lean4

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

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

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

Разделы

Аффилиация

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