completeSpace_ker — Mathlib

English

If two continuous linear maps are equal as maps, then the eqLocus is a complete space under the given hypotheses.

Русский

Если два непрерывных линейных отображения равны как отображения, то eqLocus полно в рамках данных гипотез.

LaTeX

$$$ \text{CompleteSpace}(\text{eqLocus}(f,g)) $$$

Lean4

instance completeSpace_ker {M' : Type*} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M'] [Module R₁ M']
    [T1Space M₂] [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f : F) : CompleteSpace (ker f) :=
  (isComplete_ker f).completeSpace_coe

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