completeSpace_eqLocus — Mathlib

English

There is a canonical identification between the codRestrict of a map and the codRestrict of its underlying linear map.

Русский

Существует каноническое соответствие между codRestrict отображения и codRestrict его линейной части.

LaTeX

$$$ (f.codRestrict p h).toLinearMap = (f.toLinearMap).codRestrict p h $$$

Lean4

instance completeSpace_eqLocus {M' : Type*} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M'] [Module R₁ M']
    [T2Space M₂] [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f g : F) :
    CompleteSpace (LinearMap.eqLocus f g) :=
  IsClosed.completeSpace_coe (hs := isClosed_eq (map_continuous f) (map_continuous g))

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