English
The type of all functions X → Y with prescribed values for all x' ≠ x is equivalent to the codomain Y.
Русский
Тип всех функций X → Y с заданными значениями для всех x' ≠ x эквивалентен кодом Y.
LaTeX
$$$\\{ g : X \\to Y \\;\\mid\\; g \\circ (\\uparrow) = f \\} \\simeq Y$$$
Lean4
/-- The type of all functions `X → Y` with prescribed values for all `x' ≠ x`
is equivalent to the codomain `Y`. -/
def subtypeEquivCodomain (f : { x' // x' ≠ x } → Y) : { g : X → Y // g ∘ (↑) = f } ≃ Y :=
(subtypePreimage _ f).trans <|
@funUnique { x' // ¬x' ≠ x } _ <|
show Unique { x' // ¬x' ≠ x } from
@Equiv.unique _ _
(show Unique { x' // x' = x } from { default := ⟨x, rfl⟩, uniq := fun ⟨_, h⟩ => Subtype.val_injective h })
(subtypeEquivRight fun _ => not_not)
