sliceRight_coe — Mathlib

English

If the germ of f at (x:X) is constant, then the germ of the composed function f∘Subtype.val on a subtype s is also constant.

Русский

Если герм функции f в точке x является константой, то герм композиции f∘Subtype.val на подтипе s тоже константен.

LaTeX

$$$\text{If } (f : \mathrm{Germ}(\mathcal N (x:X)) Y).IsConstant, \text{ then } ((f \circ \mathrm{Subtype.val} : s \to Y) : \mathrm{Germ}(\mathcal N x) Y).IsConstant$$$

Lean4

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

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