Theorems · Definition · functional analysis

CompactlySupportedContinuousMap.pullback_monoidHom

{α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : TopologicalSpace α] →
        [R1Space α] →
          [inst_2 : Group α] →
            [inst_3 : TopologicalSpace β] →
              [R1Space β] →
                [inst_5 : Group β] →
                  [ContinuousMul β] →
                    [inst_7 : NormedAddCommGroup γ] →
                      {φ : α →* β} →
                        Topology.IsClosedEmbedding ⇑φ →
                          CompactlySupportedContinuousMap β γ → β → CompactlySupportedContinuousMap α γ

Pull back a continuous compactly supported function f on β along a closed embedding φ : α →* β to the continuous compactly supported function a ↦ f (b * φ a) on A.

Defined in

Mathlib.Topology.ContinuousMap.CompactlySupported

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceR1SpaceGroupTopologicalSpaceR1SpaceGroupContinuousMulNormedAddCommGroup