coe_comp

Mathlib.Topology.Algebra.ContinuousAffineMap

URI: https://scilib.ai/kg/mathlib#ContinuousAffineMap.coe_comp

English

The function underlying the composed map equals the composition of the underlying functions.

Русский

Функция, лежащая в основе составной карты, равна композиции функций-оснований.

LaTeX

$$$\text{coe}(f\circ g) = f \circ g$$$

Lean4

@[simp, norm_cast]
theorem coe_comp (f : Q →ᴬ[R] Q₂) (g : P →ᴬ[R] Q) : ⇑(f.comp g) = f ∘ g :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru