coe_compLeft

Mathlib.Topology.ContinuousMap.CompactlySupported

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

English

Given hg: g(0)=0, the compactly supported composition f.compLeft g equals g ∘ f as maps.

Русский

При hg: g(0)=0 композиция f.compLeft g равна как отображение g ∘ f.

LaTeX

$$$ f.compLeft g = g \circ f $$$

Lean4

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

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

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

Разделы

Аффилиация

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