instCoeFunDividedPowersForallNatForall

English

There is a canonical coercion to regard a divided powers structure as a function so that dpow n is a map from A to A for each n.

Русский

Существует каноническая редукция к функции: для каждой n, dpow n задаёт отображение A → A.

LaTeX

$$$$ (\\text{DividedPowers } I) \\to (\\mathbb{N} \\to A \\to A) $$$$

Lean4

/-- The coercion from the divided powers structures to functions -/
instance : CoeFun (DividedPowers I) fun _ ↦ ℕ → A → A :=
  ⟨fun hI ↦ hI.dpow⟩

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