English
The inverse of the codomain correspondence sends a value y ∈ Y to a function on X that agrees with f off x and takes the value y at x. Concretely, ((subtypeEquivCodomain f).symm y)(x') = if x' ≠ x then f⟨x', h⟩ else y, where h is a witness that x' ≠ x.
Русский
Обратное отображение сопоставления подтипа преобразует значение y ∈ Y в функцию на X, согласованную с f вне x и принимающую значение y в x. Конкретно, ((subtypeEquivCodomain f).symm y)(x') = if x' ≠ x то f⟨x', h⟩, иначе y, где h — доказательство x' ≠ x.
LaTeX
$$$((\\operatorname{subtypeEquivCodomain}(f))^{-1} y)(x') = \\begin{cases} f(\\langle x', h \\rangle), & x' \\neq x \\\\ y, & x' = x \\end{cases}$$$
Lean4
theorem coe_subtypeEquivCodomain_symm (f : { x' // x' ≠ x } → Y) :
((subtypeEquivCodomain f).symm : Y → _) = fun y => ⟨fun x' => if h : x' ≠ x then f ⟨x', h⟩ else y, by grind⟩ :=
rfl
