prodMk — Mathlib

English

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

Русский

Пусть f: X → Y и f': X → Y' локально константны; тогда отображение x ↦ (f(x), f'(x)) локально константно.

LaTeX

$$$IsLocallyConstant f \to IsLocallyConstant f' \to IsLocallyConstant (\lambda x, (f x, f' x))$$$

Lean4

theorem prodMk {Y'} {f : X → Y} {f' : X → Y'} (hf : IsLocallyConstant f) (hf' : IsLocallyConstant f') :
    IsLocallyConstant fun x => (f x, f' x) :=
  (iff_eventually_eq _).2 fun x => (hf.eventually_eq x).mp <| (hf'.eventually_eq x).mono fun _ hf' hf => Prod.ext hf hf'

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