instNormedAddCommGroup

Mathlib.Analysis.Normed.Group.Completion

URI: https://scilib.ai/kg/mathlib#UniformSpace.Completion.instNormedAddCommGroup

Lean4

instance [SeminormedAddCommGroup E] : NormedAddCommGroup (Completion E) where
  dist_eq x
    y := by
    induction x, y using Completion.induction_on₂
    · refine isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous ?_
      exact Continuous.comp Completion.continuous_extension continuous_sub
    · rw [← Completion.coe_sub, norm_coe, Completion.dist_eq, dist_eq_norm]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru