restrict₂_comp_restrict₂ — Mathlib

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

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