instNormedAddCommGroup — Mathlib

English

Convergence in C0 is equivalent to convergence in the induced bounded map space via toBCF.

Русский

Сходимость в C0 эквивалентна сходимости в индуцированном пространстве ограниченных отображений через toBCF.

LaTeX

$$TendstoEquivalentViaToBCF$$

Lean4

noncomputable instance instNormedAddCommGroup [NormedAddCommGroup β] : NormedAddCommGroup C₀(α, β) :=
  fast_instance%NormedAddCommGroup.induced _ _ (⟨⟨toBCF, rfl⟩, fun _ _ => rfl⟩ : C₀(α, β) →+ α →ᵇ β)
      (toBCF_injective α β)

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