continuous_mulSingle — Mathlib

English

For each i with One(A_i) and DecidableEq ι, the map x ↦ Pi.mulSingle i x as a function ∀ i, A_i is continuous.

Русский

Для фиксированного i функция x ↦ Pi.mulSingle i x, рассматриваемая как элемент ∀ i, A_i, непрерывна.

LaTeX

$$$\text{Continuous}(\lambda x, (\Pi i, A_i).\, \operatorname{mulSingle}(i,x))$$$

Lean4

/-- `Pi.mulSingle i x` is continuous in `x`. -/
@[to_additive (attr := continuity) /-- `Pi.single i x` is continuous in `x`. -/
    ]
theorem continuous_mulSingle [∀ i, One (A i)] [DecidableEq ι] (i : ι) :
    Continuous fun x => (Pi.mulSingle i x : ∀ i, A i) :=
  continuous_const.update _ continuous_id

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