copy_eq — Mathlib

English

Let f be a Heyting homomorphism and f' a function with f' = f. Then the copy of f using f' is equal to f, i.e., f.copy f' h = f.

Русский

Пусть f — гомоморфизм Хейтинга, а f' — произвольная функция с условием f' = f. Тогда копия f с опорой на f' равна f, то есть f.copy f' h = f.

LaTeX

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

Lean4

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

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