toRealLinearEquiv — Mathlib

English

Let e: E ≃+ F be a continuous additive equivalence with continuous inverse. Then e induces a continuous real-linear equivalence E ≃ℝ F.

Русский

Пусть e: E ≃+ F является непрерывной аддитивной эквивалентностью с непрерывной обратной. Тогда e индукирует непрерывную вещественно-линейную эквиваленцию E ≃ℝ F.

LaTeX

$$$\\text{There exists a continuous real-linear bijection } E \\xrightarrow{\\mathbb{R}} F \\text{ whose underlying map agrees with } e.$$$

Lean4

/-- Reinterpret a continuous additive equivalence between two real vector spaces
as a continuous real-linear map. -/
def toRealLinearEquiv (e : E ≃+ F) (h₁ : Continuous e) (h₂ : Continuous e.symm) : E ≃L[ℝ] F :=
  { e, e.toAddMonoidHom.toRealLinearMap h₁ with }

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