English
If s is a subset of t, the restriction operator restrict₂ along hst acts by composing with the canonical inclusion: for any f, (restrict₂ hst)(f) evaluated at x equals f(⟨x.1, hst x.2⟩).
Русский
Если s ⊆ t, оператор restrict₂ по отношению к hst действует путём композиции с каноническим включением: для любого f значение (restrict₂ hst)(f) в точке x равно f(⟨x.1, hst x.2⟩).
LaTeX
$$$\\operatorname{restrict}_2(hst) = \\lambda f\\, x \\mapsto f\\langle x.1,\\; hst\\,x.2\\rangle.$$$
Lean4
theorem restrict₂_def (hst : s ⊆ t) : restrict₂ (π := π) hst = fun f x ↦ f ⟨x.1, hst x.2⟩ :=
rfl