concat_right — Mathlib

English

In the right subinterval regime, the concatenation agrees with the right piece on the overlap boundary.

Русский

правая часть сцепления совпадает с правой частью на границе пересечения.

LaTeX

$$concat_right: if f⊤ = g⊥, then (f\\concat g)(t)=g(t) for t in [b,c], via ht condition.$$

Lean4

@[simp]
theorem concat_right (hb : f ⊤ = g ⊥) {t : Icc a c} (ht : b ≤ t) : concat f g t = g ⟨t, ht, t.2.2⟩ :=
  by
  nth_rewrite 2 [← concat_comp_IccInclusionRight hb]
  rfl

Похожие утверждения