continuousSemilinearEquivClass — Mathlib

English

The constructor ContinuousLinearEquiv.mk yields a continuous linear equivalence with the given linear part and continuity data, and its coe to a map is the underlying linear equivalence.

Русский

Конструктор ContinuousLinearEquiv.mk задаёт непрерывную линейную эквиваленцию с заданной линейной частью и непрерывностью, и её отображение совпадает с базовой линейной эквивалентностью.

LaTeX

$$$ (\text{ContinuousLinearEquiv.mk } e a b)^{\nobreakspace} = e $$$

Lean4

instance continuousSemilinearEquivClass : ContinuousSemilinearEquivClass (M₁ ≃SL[σ₁₂] M₂) σ₁₂ M₁ M₂
    where
  map_add f := f.map_add'
  map_smulₛₗ f := f.map_smul'
  map_continuous := continuous_toFun
  inv_continuous := continuous_invFun

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