evalCLM_apply — Mathlib

English

There is a canonical equality between the function underlying toContinuousMapHom and the evaluation-of-function representation, i.e., the coe of toContinuousMapHom coincides with the expected function.

Русский

Существует каноничное равенство между базовым отображением toContinuousMapHom и представлением через функцию; копирование совпадает с ожидаемой функцией.

LaTeX

$$$\\text{coe\_toContinuousMapHom} : \\text{toContinuousMapHom} = \\text{Id}$$$

Lean4

@[simp]
theorem evalCLM_apply {𝕜 : Type*} [Semiring 𝕜] [Module 𝕜 R] [ContinuousConstSMul 𝕜 R] (x : X) (f : C(X, R)₀) :
    evalCLM 𝕜 x f = f x :=
  rfl

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