instCoeFunForallForall — Mathlib

English

A Flow ϕ can be viewed as a function of two variables, t ∈ τ and x ∈ α, by the rule ϕ(t)(x).

Русский

Поток ϕ можно рассматривать как функцию двух переменных: t ∈ τ и x ∈ α, задаваемую правилам ϕ(t)(x).

LaTeX

$$$\text{Flow}(\tau, \alpha) \hookrightarrow (\tau \to \alpha \to \alpha) \quad \text{via } \varphi \mapsto (t, x) \mapsto \varphi(t)(x).$$$

Lean4

instance : CoeFun (Flow τ α) fun _ => τ → α → α :=
  ⟨Flow.toFun⟩

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