ker_toContinuousLinearMap — Mathlib

English

Equality of a continuous linear map and a linear map is equivalent to equality of their corresponding linear maps.

Русский

Равенство непрерывного линейного отображения и линейного отображения эквивалентно равенству их соответствующих линейных отображений.

LaTeX

$$$g.toLinearMap = f \\;\\; \\Leftrightarrow \\;\\; g = f.toContinuousLinearMap$$$

Lean4

@[simp]
theorem ker_toContinuousLinearMap (f : E →ₗ[𝕜] F') : ker (LinearMap.toContinuousLinearMap f) = ker f :=
  rfl

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