restrictLe — Mathlib

English

Restriction of a family indexed by α to indices ≤ a is defined by restricting the domain to Iic a.

Русский

Ограничение семейства, индексируемого по α, до элементов не превосходящих a определяется как ограничение области до Iic a.

LaTeX

$$$\\text{restrictLe}(a) := (Iic(a)).\\text{restrict} (\\pi := \\pi)$$$

Lean4

/-- Restrict domain of a function `f` indexed by `α` to elements `≤ a`. -/
def restrictLe (a : α) :=
  (Iic a).restrict (π := π)

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