instTrivialStarSubtypeAEEqFunMemAddSubgroup

English

If the target has a trivial star, then the Lp space inherits a trivial star structure.

Русский

Если область значений имеет тривиальную операцию звезды, то Lp-набор также имеет тривиальный звездный структура.

LaTeX

$$$\text{TrivialStar } R \Rightarrow \text{ TrivialStar } (Lp\,R\,p\,μ)$$$

Lean4

noncomputable instance [TrivialStar R] {p : ℝ≥0∞} : TrivialStar (Lp R p μ) where
  star_trivial _ := Subtype.ext <| star_trivial _

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