continuous_restrictLe₂ — Mathlib

English

If a ≤ b in a preorder, then restricting along the pair (a,b) is continuous.

Русский

Если a ≤ b в предопорядке, то ограничение по паре (a,b) непрерывно.

LaTeX

$$$\forall a,b\;(a \le b)\;\Rightarrow\; \text{Continuous}(\operatorname{restrictLe_2}(hab)).$$$

Lean4

@[continuity, fun_prop]
theorem continuous_restrictLe₂ {a b : α} (hab : a ≤ b) : Continuous (restrictLe₂ (π := X) hab) :=
  Pi.continuous_restrict₂ _

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