English
Let X be a set, fix x ∈ X, and let Y be another set. For a function f defined on the punctured domain X \\ {x}, consider the set of all extensions g: X → Y such that g agrees with f on X \\ {x}. Then this set is in bijection with Y, via the evaluation map g ↦ g(x). Concretely, the inverse bijection sends y ∈ Y to the extension g_y with g_y(x) = y and g_y|_{X\\{x}} = f.
Русский
Пусть X — множество, фиксирована точка x ∈ X, и Y — другое множество. Пусть f задана на подмножестве X \\ {x}. Рассмотрим множество всех продолжений g: X → Y такие, что g|_{X\\{x}} = f. Тогда существует biекция между этим множеством и Y, заданная отображением g ↦ g(x). Обратное биекция отображает y ∈ Y в продолжение g_y, где g_y(x) = y и g_y|_{X\\{x}} = f.
LaTeX
$$$\\left\\{ g: X \\to Y \\mid g|_{X\\setminus\\{x\\}} = f \\right\\} \\ \\cong\\ Y,$ \\\\ $g \\mapsto g(x)$, \\\\ $y \\mapsto g_y$, where $g_y(x') = \\begin{cases} y, & x' = x \\\\ f(x'), & x' \\neq x. \\end{cases}$$$
Lean4
@[simp]
theorem coe_subtypeEquivCodomain (f : { x' // x' ≠ x } → Y) :
(subtypeEquivCodomain f : _ → Y) = fun g : { g : X → Y // g ∘ (↑) = f } => (g : X → Y) x :=
rfl
