Theorems · Definition · general topology

ContinuousMap.concat

{α : Type u_1} →
  [inst : LinearOrder α] →
    [inst_1 : TopologicalSpace α] →
      [OrderTopology α] →
        {a b c : α} →
          [Fact (a ≤ b)] →
            [Fact (b ≤ c)] →
              {E : Type u_2} →
                [inst_5 : TopologicalSpace E] → C(↑(Set.Icc a b), E) → C(↑(Set.Icc b c), E) → C(↑(Set.Icc a c), E)

The concatenation of two continuous maps defined on adjacent intervals. If the values of the functions on the common bound do not agree, this is defined as an arbitrarily chosen constant map. See concatCM for the corresponding map on the subtype of compatible function pairs.

Defined in

Mathlib.Topology.ContinuousMap.Interval

Cited by

5 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceOrderTopologyFactFactTopologicalSpace