Theorems · Definition · general topology

AddMonoidHom.compLeftContinuousBounded

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

Composition on the left by a (lipschitz-continuous) homomorphism of topological AddMonoids, as a AddMonoidHom. Similar to AddMonoidHom.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

TopologicalSpacePseudoMetricSpaceAddMonoidBoundedAddContinuousAddPseudoMetricSpaceAddMonoidBoundedAddContinuousAdd