canLiftContinuousLinearMap — Mathlib

English

Equality of the continuous linear map and a linear map is equivalent to equality of the underlying linear maps.

Русский

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

LaTeX

$$$g.toLinearMap = f \\iff g = f.toContinuousLinearMap$$$

Lean4

instance canLiftContinuousLinearMap : CanLift (E →ₗ[𝕜] F) (E →L[𝕜] F) (↑) fun _ => True :=
  ⟨fun f _ => ⟨LinearMap.toContinuousLinearMap f, rfl⟩⟩

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