continuous_frestrictLe — Mathlib

English

For locally finite orders, restricting along the finite many coordinates yields a continuous map.

Русский

При локально конечном порядке ограничение по координатам даёт непрерывное отображение.

LaTeX

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

Lean4

@[continuity, fun_prop]
theorem continuous_frestrictLe (a : α) : Continuous (frestrictLe (π := X) a) :=
  Finset.continuous_restrict _

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