Theorems · Theorem · functional analysis

CompactlySupportedContinuousMap.pullback_monoidHom_def

∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : R1Space α] [inst_2 : Group α]
  [inst_3 : TopologicalSpace β] [inst_4 : R1Space β] [inst_5 : Group β] [inst_6 : ContinuousMul β]
  [inst_7 : NormedAddCommGroup γ] {φ : α →* β} (hφ : Topology.IsClosedEmbedding ⇑φ)
  (f : CompactlySupportedContinuousMap β γ) (b : β) (a : α),
  (CompactlySupportedContinuousMap.pullback_monoidHom hφ f b) a = f (b * φ a)

Defined in

Mathlib.Topology.ContinuousMap.CompactlySupported

Cited by

1 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceR1SpaceGroupTopologicalSpaceR1SpaceGroupContinuousMulNormedAddCommGroup