coe_comp_continuousMap — Mathlib

English

The composition regarded as a continuous map equals the composition of the underlying continuous maps.

Русский

Композиция, рассматриваемая как непрерывное отображение, равна композиции соответствующих непрерывных отображений.

LaTeX

$$$ (f.comp g) \; :\text{ContinuousMap } \alpha\gamma = (f : \text{ContinuousMap } \beta\gamma) \circ (g : \text{ContinuousMap } \alpha\beta). $$$

Lean4

theorem coe_comp_continuousMap (f : SpectralMap β γ) (g : SpectralMap α β) :
    f ∘ g = (f : ContinuousMap β γ) ∘ (g : ContinuousMap α β) :=
  rfl

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