isComplete_ker — Mathlib

English

The complete space of the locus of equality of two continuous linear maps is complete when the ambient spaces are complete and appropriate topological/algebraic conditions hold.

Русский

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

LaTeX

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

Lean4

theorem isComplete_ker {M' : Type*} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M'] [Module R₁ M'] [T1Space M₂]
    [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f : F) : IsComplete (ker f : Set M') :=
  (isClosed_ker f).isComplete

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