comp₂ — Mathlib

English

For hf: EventuallyConst f l, op: β → γ → δ, and hg: EventuallyConst g l, then EventuallyConst (λx. op (f x) (g x)) l.

Русский

Для hf: EventuallyConst f l, op: β → γ → δ и hg: EventuallyConst g l, тогда EventuallyConst(λx. op (f x) (g x)) l.

LaTeX

$$$\mathrm{EventuallyConst}(f,l) \rightarrow \forall op, \mathrm{EventuallyConst}(\lambda x. op (f x) (g x), l)$$$$

Lean4

theorem comp₂ {g : α → γ} (hf : EventuallyConst f l) (op : β → γ → δ) (hg : EventuallyConst g l) :
    EventuallyConst (fun x ↦ op (f x) (g x)) l :=
  ((hf.prod hg).map op.uncurry).anti <| (tendsto_map (f := op.uncurry)).comp (tendsto_map.prodMk tendsto_map)

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