instCompleteSpaceSubtypeMemStarSubalgebra

English

There is a complete-space instance on elemental subalgebras, inherited from the ambient closure.

Русский

Для элементальных подалгебр существует структура полного пространства, наследуемая от окружающего замыкания.

LaTeX

$$CompleteSpace (elemental R x)$$

Lean4

instance {A : Type*} [UniformSpace A] [CompleteSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A]
    [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) : CompleteSpace (elemental R x) :=
  isClosed_closure.completeSpace_coe

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