coe_single

Mathlib.Topology.PartitionOfUnity

URI: https://scilib.ai/kg/mathlib#BumpCovering.coe_single

English

For a single bump covering, the coercion to a function equals the Pi.single function.

Русский

Для единственного покрытия соответствие к функции равно Pi.single.

LaTeX

$$$$ \text{coe}(\text{single } i\, s) = \Pi\text{-single } i\, 1. $$$$

Lean4

@[simp]
theorem coe_single (i : ι) (s : Set X) : ⇑(BumpCovering.single i s) = Pi.single i 1 := by rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru