restrict₂ — Mathlib

English

If s ⊆ t, restricting a family of values indexed by t to s gives a function on s.

Русский

Если s ⊆ t, ограничение семейства значений, индексируемых t, до s даёт функцию на s.

LaTeX

$$$\\text{restrict}_2 (\\,\\text{hst}: s \\subseteq t\\,) (f: ∀ a: t, π a) : ∀ a: s, π a$$$

Lean4

/-- If a function `f` is restricted to a set `t`, and `s ⊆ t`, this is the restriction to `s`. -/
@[simp]
def restrict₂ {s t : Set α} (hst : s ⊆ t) (f : ∀ a : t, π a) : ∀ a : s, π a := fun x => f ⟨x.1, hst x.2⟩

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