continuous_frestrictLe₂ — Mathlib

English

For a comparable pair a ≤ b, the two-coordinate restriction is continuous.

Русский

Для сопоставимой пары a ≤ b ограничение по двум координатам непрерывно.

LaTeX

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

Lean4

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

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