English
A partition of unity on a set s is represented by a family {f_i}_{i∈ι} of real-valued continuous functions on X, indexed by ι, so that each f_i is nonnegative and the family yields the constant function 1 on s when summed. Equivalently, the data f_i can be viewed as a function i ↦ f_i with f_i ∈ C(X, R).
Русский
Разбиение единства на множество s задаётся семейством {f_i}_{i∈ι} вещественно-значных непрерывных функций на X, индексированным по ι, причём каждый f_i неотрицателен, а сумма по i даёт константу 1 на s. По существу данные f_i представляются как функция i ↦ f_i с f_i ∈ C(X, R).
LaTeX
$$$f \in \mathrm{PartitionOfUnity}_{ι}(X,s) \quad\Longrightarrow\quad (i \mapsto f_i) : ι \to C(X, \mathbb{R}) \,\text{ with } f_i \in C(X, \mathbb{R}) \text{ for all } i.$$$
Lean4
instance : FunLike (PartitionOfUnity ι X s) ι C(X, ℝ)
where
coe := toFun
coe_injective' f g h := by cases f; cases g; congr
