continuous_toPOUFun — Mathlib

English

For every i, the i-th component of the partition of unity is a continuous function.

Русский

Для каждого i компонент разложения по единице является непрерывной функцией.

LaTeX

$$$\forall i:\, ι,\; \text{Continuous}(f^{\mathrm{POU}}_i)$$$

Lean4

theorem continuous_toPOUFun (i : ι) : Continuous (f.toPOUFun i) :=
  by
  refine (f i).continuous.mul <| continuous_finprod_cond (fun j _ => continuous_const.sub (f j).continuous) ?_
  simp only [mulSupport_one_sub]
  exact f.locallyFinite

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