restrict₂_def — Mathlib

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

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