English
The process of concatenating a net of maps on adjacent intervals converges to the concatenation of limit maps, provided the endpoints match and appropriate compactness conditions hold.
Русский
Процесс конкатенации сетки отображений на смежных интервалах сходится к конкатенации пределов отображений при заданных условиях совместимости концов и компактности.
LaTeX
$$Tendsto_concat: (F,G) → concat F G tends to concat f g under endpoint-equality and compact-open hypotheses.$$
Lean4
theorem concat_comp_IccInclusionRight (hb : f ⊤ = g ⊥) : (concat f g).comp IccInclusionRight = g :=
by
ext ⟨x, hx⟩
obtain rfl | hxb := eq_or_ne x b
· simpa [concat, IccInclusionRight, IccExtendCM, projIccCM, inclusion, hb]
· have h : ¬x ≤ b := lt_of_le_of_ne hx.1 (Ne.symm hxb) |>.not_ge
simp [concat, hb, IccInclusionRight, h, IccExtendCM, projIccCM, projIcc, inclusion, hx.2, hx.1]
