subtypeEquivCodomain_symm_apply — Mathlib

English

For a fixed x ∈ X and f: {x' // x' ≠ x} → Y, and y ∈ Y, the symm map yields a function on X given by the rule g_y(x') = f ⟨x', h⟩ if x' ≠ x, and g_y(x) = y.

Русский

Для фиксированного x ∈ X и f: {x' | x' ≠ x} → Y и y ∈ Y, симметричное отображение даёт функцию g_y на X: g_y(x') = f ⟨x', h⟩ при x' ≠ x, и g_y(x) = y.

LaTeX

$$$((\\operatorname{subtypeEquivCodomain}(f))^{-1} y)(x') = \\begin{cases} f(\\langle x', h \\rangle), & x' \\neq x \\\\ y, & x' = x \\end{cases}$$$

Lean4

@[simp]
theorem subtypeEquivCodomain_symm_apply (f : { x' // x' ≠ x } → Y) (y : Y) (x' : X) :
    ((subtypeEquivCodomain f).symm y : X → Y) x' = if h : x' ≠ x then f ⟨x', h⟩ else y :=
  rfl

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