prodMk — Mathlib

English

If hf: EventuallyConst f l and hg: EventuallyConst g l, then EventuallyConst (x ↦ (f x, g x)) l.

Русский

Если hf: EventuallyConst f l и hg: EventuallyConst g l, то EventuallyConst (x ↦ (f x, g x)) l.

LaTeX

$$$\mathrm{EventuallyConst}(f,l) \land \mathrm{EventuallyConst}(g,l) \Rightarrow \mathrm{EventuallyConst}(\lambda x. (f x, g x), l)$$$

Lean4

theorem prodMk {g : α → γ} (hf : EventuallyConst f l) (hg : EventuallyConst g l) :
    EventuallyConst (fun x ↦ (f x, g x)) l :=
  hf.comp₂ Prod.mk hg

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