English
If s ⊆ t and t ⊆ u, then composing two restrict₂ maps equals the single restrict₂ with the composed inclusion: (restrict₂ hst) ∘ (restrict₂ htu) = restrict₂ (hst.trans htu).
Русский
Если s ⊆ t ⊆ u, то композиция двух restrict₂ равна единственному restrict₂ по составному включению: (restrict₂ hst) ∘ (restrict₂ htu) = restrict₂ (hst.trans htu).
LaTeX
$$$(\\operatorname{restrict}_2(hst)) \\circ (\\operatorname{restrict}_2(htu)) = \\operatorname{restrict}_2(hst.trans(htu)).$$$
Lean4
theorem restrict₂_comp_restrict₂ (hst : s ⊆ t) (htu : t ⊆ u) :
(restrict₂ (π := π) hst) ∘ (restrict₂ htu) = restrict₂ (hst.trans htu) :=
rfl