restrict — Mathlib

English

For any family f: γ → α →ₛ β, the evaluation at a of the Finset supremum s.sup f equals the Finset supremum of the evaluations: (s.sup f) a = s.sup (λ c, f c a).

Русский

Для семейства функций f: γ → α →ₛ β справедливо то же соотношение: (s.sup f) a = sup_{c∈s} f(c) a.

LaTeX

$$$\\text{(s.sup f)}(a) = \\sup_{c \\in s} f(c)(a).$$$

Lean4

/-- Restrict a simple function `f : α →ₛ β` to a set `s`. If `s` is measurable,
then `f.restrict s a = if a ∈ s then f a else 0`, otherwise `f.restrict s = const α 0`. -/
def restrict (f : α →ₛ β) (s : Set α) : α →ₛ β :=
  if hs : MeasurableSet s then piecewise s hs f 0 else 0

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