toContinuousMap_coe — Mathlib

English

A continuous affine map, viewed as a continuous map, is equal to its toContinuousMap.

Русский

Непрерывный аффинный отображатель, рассматриваемый как непрерывное отображение, равен своему toContinuousMap.

LaTeX

$$$@[simp]\; f : P \toᴬ[R] Q \Rightarrow f.toContinuousMap = ⟨f, f.cont⟩$$$

Lean4

@[simp]
theorem toContinuousMap_coe (f : P →ᴬ[R] Q) : f.toContinuousMap = ↑f :=
  rfl

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