apply — Mathlib

English

If h: EventuallyConst g l, then for any i, EventuallyConst (g · i) l.

Русский

Если g константен вдоль l, то для любого индекса i функция x ↦ g(x)(i) остается константной вдоль l.

LaTeX

$$$\mathrm{EventuallyConst}(g,l) \Rightarrow \forall i, \mathrm{EventuallyConst}(\lambda x. g(x,i), l)$$$

Lean4

theorem apply {ι : Type*} {p : ι → Type*} {g : α → ∀ x, p x} (h : EventuallyConst g l) (i : ι) :
    EventuallyConst (g · i) l :=
  h.comp <| Function.eval i

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