ofLinearIsometry — Mathlib

English

Another formulation of the continuity preservation under composition with a linear isometry.

Русский

Ещё одно формулирование сохранения непрерывности при композиции с линейной изометрией.

LaTeX

$$Iff (Continous (f ∘ e)) (Continuous f)$$

Lean4

/-- If a linear isometry has an inverse, it is a linear isometric equivalence. -/
def ofLinearIsometry (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : f.toLinearMap.comp g = LinearMap.id)
    (h₂ : g.comp f.toLinearMap = LinearMap.id) : E ≃ₛₗᵢ[σ₁₂] E₂ :=
  { toLinearEquiv := LinearEquiv.ofLinear f.toLinearMap g h₁ h₂
    norm_map' := fun x => f.norm_map x }

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