instTrivialStar — Mathlib

English

If the target has a trivial star operation, then the space of continuous maps from α to β also carries a trivial star operation, defined pointwise by applying the star on β to the values. In particular, TrivialStar(C(α,β)) holds when TrivialStar(β) holds.

Русский

Если у β имеется тривиальная операция звезды, то множество непрерывных отображений α → β также имеет тривиальную операцию звезды, определяемую построчно: звезда f для функции f применяется по значению в каждой точке. В частности, TrivialStar(C(α,β)) при условии TrivialStar(β).

LaTeX

$$$\mathrm{TrivialStar}\bigl(C(\alpha, \beta)\bigr)$$

Lean4

instance instTrivialStar [TrivialStar β] : TrivialStar C(α, β) where star_trivial _ := ext fun _ => star_trivial _

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