copy_eq — Mathlib

English

Let f be a LocallyBoundedMap α → β and let f′ : α → β with h : f′ = f. Then the copy of f with f′ and h is equal to f, i.e., f.copy f′ h = f.

Русский

Пусть f — локально ограниченное отображение α → β и f′ : α → β таково, что f′ = f. Тогда копия f, полученная по f′ и доказательству h, равна f: f.copy f′ h = f.

LaTeX

$$$\\forall f : \\operatorname{LocallyBoundedMap}\\ \alpha \\beta \\ , \\forall f' : \\alpha \\to \\beta \\ , \\forall h : f' = f, \\ f.copy \\ f' \\ h = f.$$$

Lean4

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

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