sliceLeft — Mathlib

English

The germ of a function f: X×Y→Z at (x,y) when sliced left produces the germ of the function x↦f(x,y) at x.

Русский

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

LaTeX

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

Lean4

/-- Map the germ of functions `X × Y → Z` at `p = (x,y) ∈ X × Y` to the corresponding germ
  of functions `X → Z` at `x ∈ X` -/
def sliceLeft [TopologicalSpace Y] {p : X × Y} (P : Germ (𝓝 p) Z) : Germ (𝓝 p.1) Z :=
  P.compTendsto (Prod.mk · p.2) (Continuous.prodMk_left p.2).continuousAt

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