instTrivialStar

Mathlib.Topology.ContinuousMap.CompactlySupported

URI: https://scilib.ai/kg/mathlib#CompactlySupportedContinuousMap.instTrivialStar

English

If β has a trivial star structure, then C_c(α,β) also carries a trivial star structure, defined pointwise.

Русский

Если β обладает тривиальной звездой, то C_c(α,β) наследует тривиальную структуру звезды по точке.

LaTeX

$$$TrivialStar $C_c(α,β)$$$$

Lean4

instance [TrivialStar β] : TrivialStar C_c(α, β) where star_trivial f := ext fun x => star_trivial (f x)

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

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

Разделы

Аффилиация

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