sliceLeft_coe — Mathlib

English

Analogous to sliceLeft, the germ at (x,y) sliced to the right yields the germ of the function y↦f(x,y) at y.

Русский

Аналогично sliceLeft, срез справа гёрма на точке (x,y) даёт герман функции y↦f(x,y) в точке y.

LaTeX

$$$(\uparrow f : \mathrm{Germ}(\mathcal N (x,y)) Z).\mathrm{sliceRight} = \lambda y' \mapsto f(x,y')$$$

Lean4

@[simp]
theorem sliceLeft_coe [TopologicalSpace Y] {y : Y} (f : X × Y → Z) :
    (↑f : Germ (𝓝 (x, y)) Z).sliceLeft = fun x' ↦ f (x', y) :=
  rfl

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