toContinuousMapAddHom — Mathlib

English

For f,g ∈ BoundedContinuousFunction α β and h ∈ ContinuousMap γ α, we have (g+f) ∘ h = g ∘ h + f ∘ h.

Русский

Для f,g ∈ ограниченных непрерывных функций α→β и h ∈ непрерывного отображения γ→α имеем (g+f) ∘ h = g ∘ h + f ∘ h.

LaTeX

$$$((g+f) \circ h) = (g \circ h) + (f \circ h)$$$

Lean4

/-- The additive map forgetting that a bounded continuous function is bounded. -/
@[simps]
def toContinuousMapAddHom [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] : (α →ᵇ β) →+ C(α, β)
    where
  toFun := toContinuousMap
  map_zero' := rfl
  map_add' := by
    intros
    ext
    simp

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