Theorems · Definition · functional analysis

RingHom.compLeftContinuousBounded

{β : Type v} →
  {γ : Type w} →
    (α : Type u_2) →
      [inst : TopologicalSpace α] →
        [inst_1 : SeminormedRing β] →
          [inst_2 : SeminormedRing γ] →
            (g : β →+* γ) →
              {C : NNReal} → LipschitzWith C ⇑g → BoundedContinuousFunction α β →+* BoundedContinuousFunction α γ

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

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Normed

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSeminormedRingSeminormedRing