isConstant_comp_subtype — Mathlib

English

Same as previous, asserting constant germ after composing with Subtype.val on a subtype.

Русский

То же самое: константный герм после композиции с Subtype.val на подтипе.

LaTeX

$${hf : (f : \mathrm{Germ}(\mathcal N (x:X)) Y).IsConstant} \Rightarrow ((f \circ \mathrm{Subtype.val} : s → Y) : \mathrm{Germ}(\mathcal N x) Y).IsConstant$$

Lean4

theorem isConstant_comp_subtype {s : Set X} {f : X → Y} {x : s} (hf : (f : Germ (𝓝 (x : X)) Y).IsConstant) :
    ((f ∘ Subtype.val : s → Y) : Germ (𝓝 x) Y).IsConstant :=
  isConstant_comp_tendsto hf continuousAt_subtype_val

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