subtypeEquivCodomain_apply — Mathlib

English

For a fixed x ∈ X and f: {x' // x' ≠ x} → Y, the forward component of the canonical bijection between extensions of f to X and functions on the punctured domain evaluates to the value of g at x. In particular, subtypeEquivCodomain f applied to g equals g(x).

Русский

Для фиксированного x ∈ X и f: {x' | x' ≠ x} → Y, диаграмма продолжений через расширение на X даёт отображение, которое от g возвращает g(x). То есть subtypeEquivCodomain f (g) = g(x).

LaTeX

$$$\\operatorname{subtypeEquivCodomain}(f)(g) = g(x)$$$

Lean4

@[simp]
theorem subtypeEquivCodomain_apply (f : { x' // x' ≠ x } → Y) (g) : subtypeEquivCodomain f g = (g : X → Y) x :=
  rfl

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