restrict₂_comp_restrict — Mathlib

English

For s ⊆ t, composing restrict₂ with t.restrict gives the same as directly restricting to s: (restrict₂ hst) ∘ t.restrict = s.restrict.

Русский

При s ⊆ t композиция restrict₂ с t.restrict равна непосредственному ограничению до s: (restrict₂ hst) ∘ t.restrict = s.restrict.

LaTeX

$$$(\\operatorname{restrict}_2(hst)) \\circ t.\\operatorname{restrict} = s.\\operatorname{restrict}.$$$

Lean4

theorem restrict₂_comp_restrict (hst : s ⊆ t) : (restrict₂ (π := π) hst) ∘ t.restrict = s.restrict :=
  rfl

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