continuous_update — Mathlib

English

For any Finset s ⊆ ι, the map s.restrict: (∀ i, A_i) → (∀ i ∈ s, A_i) is continuous.

Русский

Для любого конечного множества s ⊆ ι отображение s.restrict непрерывно.

LaTeX

$$$\text{Continuous}(s.restrict)$$$

Lean4

/-- `Function.update f i x` is continuous in `(f, x)`. -/
@[continuity, fun_prop]
theorem continuous_update [DecidableEq ι] (i : ι) : Continuous fun f : (∀ j, A j) × A i => update f.1 i f.2 :=
  continuous_fst.update i continuous_snd

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