compLeft_apply

Mathlib.Topology.ContinuousMap.CompactlySupported

URI: https://scilib.ai/kg/mathlib#CompactlySupportedContinuousMap.compLeft_apply

English

For hg: g(0)=0 and f: C_c(α,β), and a ∈ α, we have (f.compLeft g)(a) = g(f(a)).

Русский

Для hg: g(0)=0 и f: C_c(α,β), и a ∈ α, имеет место (f.compLeft g)(a) = g(f(a)).

LaTeX

$$$ (f.compLeft g) a = g (f a) $$$

Lean4

theorem compLeft_apply {g : C(β, γ)} (hg : g 0 = 0) (f : C_c(α, β)) (a : α) : f.compLeft g a = g (f a) := by
  simp [coe_compLeft hg f]

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

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

Разделы

Аффилиация

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