comp₂ — Mathlib

English

If f: X → Y and g: X → Y' are locally constant, then for any h: Y → Y' → Z, the map x ↦ h(f(x))(g(x)) is locally constant.

Русский

Если f: X → Y и g: X → Y' локально константны, то для любого h: Y → Y' → Z отображение x ↦ h(f(x))(g(x)) локально константно.

LaTeX

$$$IsLocallyConstant f \to IsLocallyConstant g \to \forall h: Y \to Y' \to Z, IsLocallyConstant (\lambda x, h (f x) (g x))$$$

Lean4

theorem comp₂ {Y₁ Y₂ Z : Type*} {f : X → Y₁} {g : X → Y₂} (hf : IsLocallyConstant f) (hg : IsLocallyConstant g)
    (h : Y₁ → Y₂ → Z) : IsLocallyConstant fun x => h (f x) (g x) :=
  (hf.prodMk hg).comp fun x : Y₁ × Y₂ => h x.1 x.2

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