toContinuousMap_compLeft

Mathlib.Topology.ContinuousMap.CompactlySupported

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

English

If g(0)=0, then for every f: C_c(α,β), the toContinuousMap of f.compLeft g equals g ∘ f.

Русский

Если g(0)=0, то для каждого f: C_c(α,β) toContinuousMap от f.compLeft g равен g ∘ f.

LaTeX

$$$ \forall f : C_c(α, β),\ (f.compLeft g).toContinuousMap = g \circ f $$$

Lean4

theorem toContinuousMap_compLeft {g : C(β, γ)} (hg : g 0 = 0) (f : C_c(α, β)) :
    (f.compLeft g).toContinuousMap = g.comp f :=
  if_pos hg

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

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

Разделы

Аффилиация

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