comp_apply

Mathlib.Analysis.Normed.Group.SemiNormedGrp

URI: https://scilib.ai/kg/mathlib#SemiNormedGrp.comp_apply

English

For f: M → N and g: N → O and r ∈ M, (f ≫ g)(r) = g(f(r)).

Русский

Для f: M → N и g: N → O и элементr ∈ M, (f ≫ g)(r) = g(f(r)).

LaTeX

$$$ (f \circ g)(r) = g(f(r)) $$$

Lean4

theorem comp_apply {M N O : SemiNormedGrp} (f : M ⟶ N) (g : N ⟶ O) (r : M) : (f ≫ g) r = g (f r) := by simp

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

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

Разделы

Аффилиация

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