continuous_restrictLe — Mathlib

English

For a fixed index a, the function sending a family X to restrictLe along a is continuous.

Русский

Для фиксированного индекса a отображение семейства X на ограничение по элементу a непрерывно.

LaTeX

$$$\forall a,\; \text{Continuous}(\operatorname{restrictLe}(\pi := X), a).$$$

Lean4

@[continuity, fun_prop]
theorem continuous_restrictLe (a : α) : Continuous (restrictLe (π := X) a) :=
  Pi.continuous_restrict _

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