Theorems · Definition · general topology

MonoidHom.compLeftContinuousBounded

{β : Type v} →
  {γ : Type w} →
    (α : Type u_3) →
      [inst : TopologicalSpace α] →
        [inst_1 : PseudoMetricSpace β] →
          [inst_2 : Monoid β] →
            [inst_3 : BoundedMul β] →
              [inst_4 : ContinuousMul β] →
                [inst_5 : PseudoMetricSpace γ] →
                  [inst_6 : Monoid γ] →
                    [inst_7 : BoundedMul γ] →
                      [inst_8 : ContinuousMul γ] →
                        (g : β →* γ) →
                          {C : NNReal} →
                            LipschitzWith C ⇑g → BoundedContinuousFunction α β →* BoundedContinuousFunction α γ

Composition on the left by a (lipschitz-continuous) homomorphism of topological monoids, as a MonoidHom. Similar to MonoidHom.compLeftContinuous.

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePseudoMetricSpaceMonoidBoundedMulContinuousMulPseudoMetricSpaceMonoidBoundedMulContinuousMul