mkOfCompact_add — Mathlib

English

If α is compact and β is an additive topological group, then mkOfCompact is additive: mkOfCompact(f+g) = mkOfCompact(f) + mkOfCompact(g) for f,g ∈ C(α,β).

Русский

Если α компактно, а β — аддитивная топологическая группа, то mkOfCompact сохраняет сложение: mkOfCompact(f+g) = mkOfCompact(f) + mkOfCompact(g) для функций f,g ∈ C(α,β).

LaTeX

$$$\text{mkOfCompact}(f+g) = \text{mkOfCompact}(f) + \text{mkOfCompact}(g)$$$

Lean4

@[simp]
theorem mkOfCompact_add [CompactSpace α] [Add β] [BoundedAdd β] [ContinuousAdd β] (f g : C(α, β)) :
    mkOfCompact (f + g) = mkOfCompact f + mkOfCompact g :=
  rfl

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