coe_comp_continuousMap' — Mathlib

English

The equality between the two representations of the composition as continuous maps holds.

Русский

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

LaTeX

$$$ (f.comp g : ContinuousMap α γ) = (f : ContinuousMap β γ) \circ (g : ContinuousMap α β). $$$

Lean4

@[simp]
theorem coe_comp_continuousMap' (f : SpectralMap β γ) (g : SpectralMap α β) :
    (f.comp g : ContinuousMap α γ) = (f : ContinuousMap β γ).comp g :=
  rfl

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