continuous_restrict₂ — Mathlib

English

For s ⊆ t and a continuous f : t → Z, the restriction Finset.restrict₂ hst f is continuous.

Русский

Для s ⊆ t и непрерывного f : t → Z, ограничение Finset.restrict₂ hst f непрерывно.

LaTeX

$$$\text{Continuous}(\operatorname{restrict_2}(\text{hst},f))$$$

Lean4

@[continuity, fun_prop]
theorem continuous_restrict₂ {s t : Finset ι} (hst : s ⊆ t) : Continuous (Finset.restrict₂ (π := A) hst) :=
  continuous_pi fun _ ↦ continuous_apply _

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