English
The concatenation CM operator on pairs of maps is defined by applying concat to the pair's components after establishing the compatibility condition on their top and bottom elements.
Русский
оператор сцепления CM определяется применением concat к компонентам пары отображений при условии совместимости.
LaTeX
$$concatCM : maps from a compatible pair to the concatenated map on the full interval.$$
Lean4
/-- The concatenation of compatible pairs of continuous maps on adjacent intervals, defined as a
`ContinuousMap` on a subtype of the product. -/
noncomputable def concatCM : C({ fg : C(Icc a b, E) × C(Icc b c, E) // fg.1 ⊤ = fg.2 ⊥ }, C(Icc a c, E))
where
toFun fg := concat fg.val.1 fg.val.2
continuous_toFun := by
let S : Set (C(Icc a b, E) × C(Icc b c, E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
change Continuous (S.restrict concat.uncurry)
refine continuousOn_iff_continuous_restrict.mp (fun fg hfg => ?_)
refine tendsto_concat ?_ hfg ?_ ?_
· exact eventually_nhdsWithin_of_forall (fun _ => id)
· exact tendsto_nhdsWithin_of_tendsto_nhds continuousAt_fst
· exact tendsto_nhdsWithin_of_tendsto_nhds continuousAt_snd
