copy_eq — Mathlib

English

Let f be a bounded lattice homomorphism and f' any map with f' = f. Then the copy f' of f with proof h equals the original f.

Русский

Пусть f будет гомоморфизмом ограниченной решетки, а f' любая биекция с условием f' = f. Тогда копия f' с доказательством h равна исходному f.

LaTeX

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

Lean4

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

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