copy_eq — Mathlib

English

Let X and Y be topological spaces and f a continuous map considered as an element of the space of continuous maps C(X, Y). If f' is a function X → Y and h is a proof that f' = f, then the copy of f with underlying function f' coincides with f. In particular, f.copy f' h = f.

Русский

Пусть X, Y — топологические пространства, и f — непрерывное отображение X → Y. Пусть f' : X → Y и h : f' = f. Тогда копия f с опорной функцией f' равна f; то есть f.copy f' h = f.

LaTeX

$$$ f' = f \\Rightarrow f.copy\\ f'\\ h = f $$$

Lean4

theorem copy_eq (f : C(X, Y)) (f' : X → Y) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

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