coe_toComplₗᵢ — Mathlib

English

The canonical embedding into the completion, when viewed as a continuous linear map, is equal to the underlying inclusion map.

Русский

Каноническое вложение в завершение, рассматриваемое как непрерывно-линейное отображение, совпадает с базовым включением.

LaTeX

$$toComplL = inclusion$$

Lean4

@[simp]
theorem coe_toComplₗᵢ : ⇑(toComplₗᵢ : E →ₗᵢ[𝕜] Completion E) = ((↑) : E → Completion E) :=
  rfl

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